\documentclass[orivec]{llncs}

\usepackage{headers}
\usepackage{macro2}
\usepackage{xspace}
\usepackage[noend]{algpseudocode}
\usepackage{algorithm}


%opening

\title{Activity Networks with Delays}

\author{%
  Cinzia Di Giusto\inst{1} \and
  Jean-Louis Giavitto\inst{2} \and
  \\
  Hanna Klaudel\inst{1} \and
  Antoine Spicher\inst{3} 
}

\institute{%%
  IBISC, Université d'Evry - Val d'Essonne, Evry, France %
  \and %
  CNRS, IRCAM, UPMC - UMR 9912 STMS \& INRIA MuTAnt team, Paris, France 
  % 
  \and %
  LACL, Université Paris-Est, Créteil, France}

\widowpenalty=0
\clubpenalty=0

\begin{document}
\maketitle \vspace{-0.7cm}
\begin{abstract}
      \andy, Activity Networks with Delays, is a discrete time framework
      aimed to the qualitative modeling of time dependent activities.
      Each activity involves entities that may represent objects (\eg
      agents, bio-chemical species or families of thereof) with a
      local state denoting  its level (\eg concentrations, strength, expression
      levels). Thus, an \andy global state involves a set of entities at
      their respective level.

      System dynamics corresponds to %both synchronous and asynchronous
      evolution of entities' levels specified by a set of rules called
      activities. Activities involve entities that can play the role of
      activators, inhibitors or results in a static influence network.
      Activities may have given durations: they can take place only if
      all activators are available at a given level and all inhibitors
      are not present for the whole duration of the activity. Depending
      on the type of the activity, updates of levels achieve aging,
      degradation or other time dependent processes.

      We define the model formally with high-level Petri nets.
			%and illustrate it with examples coming from various domains. 
			We show
      that  \andy's concept of time has a counterpart in timed
      automata.  The encoding is however non trivial and above all
      exponential thus limiting the use of this representation in
      practice.  Nevertheless, the theoretical foundation of \andy makes
      possible the analysis and the exploration of its behavior through
      model-checking techniques.
\end{abstract}
 
\section{Introduction}

Activities are a central concern in many domains such as business (workflows, supply chains), transaction modeling (database transactions, web services) or biochemical systems (signaling networks, regulatory pathways).
%, to mention some. 
These activity-driven domains, although quite different, share foundational principles that concern, in general, two dimensions: i) control-flow  and ii) control-data factors. 
Control-flow  refers to the causal relationships
 among activities, when they can be performed, how long does it take to complete an activity, if they must be performed with time progression or if they can be delayed or even ignored. 
Control-data, instead,  addresses how data can play a role in promoting or  preventing an activity. For instance, in biochemistry, data may be represented by  species which may act as reactants or inhibitors of reactions (activities).\looseness=-1

Here  we propose a framework devoted to the modeling and the analysis of  activity-driven domains. 
%The starting point of our proposal is inspired by  
Our proposal stems from reaction systems %as defined in 
\cite{DBLP:journals/ijfcs/BrijderEMR11}. Such systems are composed of a set of \emph{reactions},
each of them defined as a triple $(R, I, P)$ with $R$  set of
\emph{reactants}, $I$  set of \emph{inhibitors} and $P$  set of
\emph{products}, and $R,I$ and $P$  taken from a common set of
\emph{species}. Reaction systems are based on three foundational
principles:
%\begin{enumerate}[1.]
% \item \label{item:react} 
(i) a reaction can take place only if all the reactants involved are available but none of the inhibitors is; 
 %\item \label{item:quantity} 
(ii) if a species is available then a sufficient amount of it is present to trigger a reaction; 
% \item 
(iii) species are not persistent: they become unavailable if they are not sustained by a reaction.
%\end{enumerate}

We complement this model by adding features to both control-flow and control-data dimensions. 
From the control-flow perspective, we add a way to directly express reaction durations (\ie the time required to yield products) and from the control-data point of view we extend previous the framework by refining the notion of species, thus allowing the construction of richer forms of reactions (\eg a state of a species can play both roles of reactant and inhibitor in the same activity). So, from reaction systems we retained the core of reactions (that we call \emph{activities}), we specialize species (here called \emph{entities}) with expression levels and we introduce time constraints.

The resulting formalism \andy, which stands for Activity Networks with Delays, targets systems
composed of various \emph{entities}: actors, agents or
families of thereof that evolve by means of time dependent activities. Each entity is characterized by one attribute,
called \emph{level}, representing rates, thresholds of activation/inhibition or expression degrees
(\eg low, medium, high). 
A system evolution shows how entities levels change along time as result of  activities. 
\emph{Activities} are rules involving three sets of entities:
\emph{activators}, which must be present, 
\emph{inhibitors}, which must be absent,  and \emph{results}.
Depending of their kind, \emph{mandatory} or \emph{\potential,}
activities must or may be activated producing possibly a change of
entities levels in the results set.  

The introduction of time concerns both activities and entities. Activities have a duration and entities are subject
to a \emph{decay} process or aging that models the action of a
non-specified environment: levels decrease with time
progression.
%%
As, in our modeling, all entities share the same global clock, it is reasonable to assume to work with discrete time constraints \cite{Wang04formalverification}. 




% An entity, also called observable or variable in
% other context, represents a (qualitatively) measurable property of the
% system.
%%








% 
% 
% Our initial objective is to provide effective tools for the
% description and then the understanding of the mechanisms and of the
% structural properties underpinning interactions networks, such as
% biochemical systems, signaling networks or regulatory pathways. In
% this area, ordinary differential equations (ODE) remain the
% predominant modeling methodology. Such models present however some
% drawbacks:
% %%
% they require simplifying assumptions (\eg spatially uniform
% concentration) as well as the exact value of numerous parameters, %
% random interactions are difficult to model outside an averaged
% approach, %
% system openness and non-linearities make hopeless the existence of
% analytic solutions, %
% and numerical methods -- often the only sensible option -- are mainly
% descriptive and cannot form the basis for an explanatory theory.
% 
% 
% 
% On the other hand, Computer Science has developed (or appropriated) many
% languages and tools to help build and explore discrete qualitative
% models in various application domains. Such models are rough
% abstractions of real world processes but they make possible to unravel
% the entangled causal relationships between system's entities.
% %%
% More specifically in systems biology, formalisms like Petri
% nets~\cite{ChaouillaThieffry}, boolean networks~\cite{thomas1973boolean},
% process algebra~\cite{journals/tcsb/Cardelli05} or rewriting
% systems~\cite{giavitto04a} (to cite a few) have been used with
% undeniable successes to understand the causal links between structure
% and behavior in molecular networks.
% 
% Nonetheless, the management of time is somewhat problematic in all of
% the previous examples. For example, it is difficult to specify both
% synchronous and asynchronous activities. A notion of ``rate of
% activity'' is hard to express, if not impossible. And the management of
% delays and duration is cumbersome.
% 
% 
% In this paper, we propose \andy, a new formalism based on the notion of
% activity network devoted to the qualitative modular modeling of
% time-depending systems. Activity networks have proven useful in the
% modeling of molecular networks~\cite{} and we extend them to take into
% account a more expressive management of time.
% %%



%\paragraph
\noindent{\bf Organization of the paper.} 
The paper is organized as follows: 
%%
Section \ref{sec:reaction} introduces the principles behind \andy
networks through the modeling of a mobile phone battery. This example
shows the versatility of the \andy formalism: initiated for modeling
application in system's biology we believe that \andy is able to model
activity-driven domains. %workflow, supply chain, coordination of web services, etc.
%%
Next, Section \ref{sec:petri} gives a formal definition of \andy
constructions in terms of high-level Petri nets.
%%
The resulting Petri net is compact and provides an intelligible
graphical representation of the described activities. Moreover, the
network is easily scalable: the size of the network grows linearly with
the number of added entities and activities. 
%%
Section \ref{sec:timedauto} presents an alternative translation of \andy
networks into a suitable class of timed automata. This translation
clarifies the semantics of delays and durations and asses the handling
of \andy's temporal concepts in a suitable and well known framework. The
encoding of an \andy network into a timed automata is exponential,
showing the expressive relevance and the concision of the original
\andy's notation.
%%
Finally, Section \ref{sec:concl} discusses related works and concludes
with some perspectives opened by the first simulation and model-checking
tools developed for \andy.




%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Constitutive Elements of \andy}\label{sec:reaction}

In this section we describe the syntax and sketch informally the
semantics of \emph{Activity Networks with Delays} (\andy). 
In order to illustrate the main features of \andy, we consider the following running example: 
\begin{example}[Mobile phone battery] \label{ex:battery} %
      Take the battery of a mobile phone.  We identify its
      electric capacity as an entity having a few charge levels. For the
      sake of the example, say $5$ levels from $0$ the minimal level of
      charge to $4$ meaning full charge. The evolution of the charge
      level along time is subject to the following constraints:
      \begin{enumerate}

      \item \label{it:decay} The level of mobile phone charge diminishes
            continuously, even when it is not used for making a phone
            call; it diminishes slowly when it is fully charged and
            faster when it is partly discharged;

      \item \label{it:plug} The mobile phone may be plugged to start
            charging, which takes some time to reach full charge;

      \item \label{it:call} If charged enough, the mobile phone may be
            used to make phone calls but its charge diminishes;

      \item \label{it:GPS} Similarly, GPS navigation needs more charge
            and consumes battery faster.
      \end{enumerate}
      Item~(\ref{it:decay}) corresponds to the decay process, while the
      other three items represent activity rules. Item (\ref{it:plug})
      is modeled with an auxiliary entity representing the plug (which
      may be on or off). The action of plugging the mobile phone is a
      \potential activity. If plugged the battery starts charging which
      is represented by a \obligatory activity augmenting its charge
      level. Items~(\ref{it:call}) and~(\ref{it:GPS}) are implemented
      similarly, using two more entities one for the call and the other
      for the GPS navigation. \hfill $\diamond$
\end{example}

As mentioned
in the introduction, an \andy network is composed of a set of entities
\entities governed by a set of activities.  
Entities  represent the actors of the modeled
system. They could be concrete objects or more abstract concepts such as
rates or states of an object.
%%
Entities have a finite number of levels $\setlev$ from 0 to $\setlev-1$,
in general they represent ordered expression degrees (\eg low, medium,
high) and they refer to a change in their capability of action.
Each entity $\entity \in \entities$ is initialized at a certain level
$\level{\entity}$ and each level is associated with a decay duration which
is either $\omega$ (unbounded) or a  natural number (thus allowing
different durations for different levels):
\[ 
\life_\entity:[0 \mydots \setlev_\entity-1] \to \nat^+ \cup \{\omega \}.
\]
For each entity $\entity$, we assume $\life_{\entity}(0) = \omega$.
$\life_\entity(i) \neq \omega$ indicates that the presence of the entity
at level $i$ is \emph{transient} and by effect of an unspecified
environment, it decays or ages gradually
% (\eg decrease or increase the level)  THIS GOES IN THE CONCLUSIONS
as time passes by. On the contrary, if $\life_\entity(i) =
\omega$, entity levels are \emph{permanent} and they can be modified
only by activities.
 
\begin{example}[Mobile phone battery - entities]
      %Take Example \ref{ex:battery} above.  
			A mobile phone is characterized by four observables with corresponding number of levels and associated decay:
      $$ \begin{array}{rcll}
            \text{Battery}  
            & ~~B~~ 
            & \setlev_{B} = 5
            & \life_{B}(i)=2 \text{ for }  0<i \leq 3,  \quad
            \life_{B}(4)=3
            \\
            \text{Plug} 
            & P 
            & \setlev_{P} = 2 
            &  
            \\
            \text{Call} 
            & C 
            & \setlev_{C} = 2 
            &  
            \\
            \text{GPS} 
            & G 
            & \setlev_{G} = 2 \ 
            &  
      \end{array}
      $$
      %%
      where unspecified decays are all set to $\omega$.  Decay
      durations are used to model Item (\ref{it:decay}) of the mobile
      phone behavior in Example \ref{ex:battery}. Notice that in the modeling of charge $B$,
      delays are not uniform to denote different speeds in the
      consumption of the charge (\ie for the full charge level 4 decay
      takes 3 units of time while for the others it is 2).  All other
      entities have only two levels, roughly speaking
      \emph{on}/\emph{off}, encoded as 0 for \emph{off} and 1 for
      \emph{on}. The environment has no role in the evolution of the
      levels of these observables that are therefore set to unbounded
      duration $\omega$.  \hfill $\diamond$
\end{example}


The evolution of entities is governed by a set of \emph{activities} of
the form
\begin{equation}\label{eq:reaction}
      \rho ::= \activ{A_{\rho}}{I_{\rho}}{\dur{\rho}}{R_{\rho}}
\end{equation}
where $\dur{\rho} \in \nat$ is the activity duration, $A_{\rho}$ (activators), $I_{\rho}$
(inhibitors) are sets of pairs $(\entity, \level{\entity})$ and $R_{\rho}$
(results) is a non empty set of pairs $(\entity, v)$, where $\entity\in
\entities$, $\level{\entity} \in [0 \mydots \setlev_\entity-1]$ and $v \in
\mathbb{Z}$. We write $s \in A_{\rho}$ to denote  $(s, \cdot) \in A_{\rho}$ similarly for $I_{\rho}$ and $R_{\rho}$ and we omit index $\rho$ if it is clear from the context.

%%
Duration $\dur{}$ characterizes the time required for yielding change of
levels of results, $\dur{} =0 $ denotes an instantaneous activity.
%%
The relative number $v$ is seen as an operator acting on levels to
increase or decrease it by $v$.



%\paragraph{Enabled activities.}

The sets $A$ and $I$ give a fine control over the interactions between
entities. An activity can be \emph{enabled} or \emph{disabled} following
the current level of the entities and the activator and inhibitor
thresholds that appear in the associated rule:
\begin{itemize}

\item Activator and inhibitor thresholds are \emph{inclusive}: if an
      entity $\entity$ is an activator (resp. an inhibitor) at level
      $\ell$ for some activity $\rho$, it is also an activator (resp. an
      inhibitor) for $\rho$ at all level $l \ge \ell$.

\item Observing only the current level of each entity is not enough to
decide if an activity is enabled: such approach will miss the handling
of decays and durations. 
%%
To take into account a notion of elapsed time, an activity $\rho$ is
enabled (\ie may happen) if all entities $\entity_a$ of activators
$(\entity_a, \level{a})$ are available at least at level $\level{a}$
and all entities $\entity_i$ of inhibitors $(\entity_i, \level{i})$
are expressed at a level strictly inferior to $\level{i}$ \emph{for
  the whole response time period $\dur{}$}.



\item Entities can appear at most once in each set $A$, $I$ and $R$. An
      entity may be both in $A$ and $R$, \eg as in an
      auto-catalytic production where reaction products themselves are activators for the reaction.

      \item Activators and inhibitors are not ``consumed'': to handle the consumption of an entity $\entity$ during an activity, $\entity$ must appear both in $A$ and $R$.

      
\item An entity can appear in the same activity simultaneously as an
      activator and an inhibitor. In such a case, we require them to
      occur with different levels. For instance, the rule
      $$
      \activ{\{({\entity},\level{})\} \cup A}{\{({\entity}, \level{}')\} \cup I}{\dur{}}{R}
      \qquad  \text{where~}   \level{} < \level{}'
      $$
      requires that the activity takes place only if the level
      $\lev_{\entity}$ of ${\entity}$ belongs to the interval $\level{}
      \leq \lev_{\entity} < \level{}'$. In particular, if ${\entity}$
      has to be present in an activity exactly at level $\level{}$,
      ${\entity}$ should appear as an activator at level $\level{}$ and
      as inhibitor at level $\level{}' = \level{}+1$.

      
\item The set of activators and inhibitors $A \cup I $ is allowed to be
      empty. In this case, the activity is constantly enabled. This
      accounts for modeling an environment that is continuously
      sustaining the production of an entity. In this case a duration
      $\dur{} \not= 0$ may be used to accounts for a start-up time.

\end{itemize}
%%


%\paragraph{\Obligatory and \potential activities.}
% It is important to note that when an activity is enabled, it is not
% necessarily performed. The idea is to make a distinction between

Enabled activities are of two types: 
\begin{enumerate}
\item \emph{\potential} activities, denoted $\alpha$ in a set $\Reac$:
      if enabled at some date, they \emph{may} occur and the result
      depends on the order they are performed;

\item \emph{\obligatory} activities, denoted $\beta$ in a set $\Syn$: if
      enabled at some date, they \emph{must} occur. All enabled
      \obligatory activities occur simultaneously.
\end{enumerate}



\begin{example}[Mobile phone battery - activities]
      The constraints specified by Items (2-4) in
      Example~\ref{ex:battery} give rise to the following sets of
      activities.

      Item (\ref{it:plug}) may be described by two \potential
      instantaneous activities, $\alpha_1$ and $\alpha_2$, which model
      plugging and unplugging respectively, and a \obligatory activity
      $\beta_1$ with duration 1 that models the charging process.
      $$
      \begin{array}{ll ll}
        \alpha_1: & \activ{(P,0)}{(P,1)}{0}{(P,+1)} 
        \qquad & \beta_1: & \activ{(P,1)}{\emptyset}{1}{(B,+1)}  \\
         \alpha_2: & \activ{(P,1)}{\emptyset}{0}{(P,-1)}   
      \end{array}
      $$

      Similarly, Item (\ref{it:call}) may be depicted by two
      \potential instantaneous activities, $\alpha_3$ and $\alpha_4$,
      modeling the start and the end of a phone call respectively, and
      a \obligatory activity $\beta_2$ with duration 3 defining the
      discharging process due to such a call.\looseness=-1
      %% 
      $$
      \begin{array}{ll ll}
            \alpha_3: & \activ{(C,0)}{(C,1)}{0}{(C,+1)} 
            \qquad & \beta_2: & \activ{(C,1)}{\emptyset}{3}{(B,-1)} \\
            \alpha_4: & \activ{(C,1)}{\emptyset}{0}{(C,-1)} 
      \end{array}
      $$

      Finally Item (\ref{it:GPS}) may again be described by two
      \potential instantaneous activities, $\alpha_5$ and $\alpha_6$,
      that model activation and deactivation of GPS navigation
      respectively, and a \obligatory activity $\beta_3$ with
      duration 3 that models the discharging process due to the GPS
      usage. Notice that in this case, even if duration is the same,
      the battery is consumed faster than a simple phone call
      (indicated by $(B, -2)$ instead of $(B, -1)$).
      $$
      \begin{array}{ll ll}
            \alpha_5: & \activ{(G,0)}{(G,1)}{0}{(G,+1)}
            \qquad &  \beta_3: & \activ{(G,1)}{\emptyset}{3}{(B,-2)} \\
            \alpha_6: & \activ{(G,1)}{\emptyset}{0}{(G,-1)} 
      \end{array}
      $$
      \hfill\raisebox{3mm}[0mm]{$\diamond$}
\end{example}




%\paragraph{Triggering an enabled activity.}

When an activity is enabled, it can be triggered: 
%The effect of
%triggering a rule is intuitive: 
the levels of the entities appearing in
the results are updated with the increment specified in the right hand
side of the rule. 
Moreover we assume that once triggered an activity $\rho$, must wait at least $\dur{\rho}$ before being enabled again\footnote{This is a non restrictive hypothesis and by slightly modifying Definition \ref{def:rs} one can obtain different semantics that could depend on the specific modeled scenario: \eg once enabled an activity $\rho$ can be triggered an unbounded number of times, or once enabled  $\rho$ can be triggered once per time unit.}.
%
It may happen, that several \obligatory activities $\beta_i$ referring
to the same entity $\entity$ in their results are triggered
simultaneously. In this case, all updates related to $\entity$ are
collected and summed up before being applied to the current level of
$\entity$.




% \paragraph{The dynamics of an \andy network.}
 
Summing up, an \andy network is a triple $(\entities, \Syn, \Reac)$ where
$\entities$ is the set of entities, $\Syn$ is the set of \obligatory
activities and $\Reac$ is the set of \potential ones. It evolves by triggering enabled activities in two independent phases:
\begin{enumerate}[Ph. 1]

\item \label{item:reaction} %%
      In this phase, \textbf{\potential activities} that are
      enabled may be triggered. Their action occurs in an interleaved
      way. Any potential activity is triggered at most once in this phase
      and the time does not progress. 


\item \label{item:clock} %%
      This phase is the time transition, it regards all entities.
      We register the progression of time with related
      decay of concerned entities and all enabled \textbf{\obligatory
        activities} are performed simultaneously.
      %% 
      Notice that as activators and inhibitors are not consumed, there
      are no conflicts and so there is a unique way (per time unit) to
      execute all enabled \obligatory activities.
\end{enumerate}





\begin{example}[Mobile phone battery - initial state and execution
      scenario]
			\label{ex:intuitive_scenario}
We illustrate the functioning of an \andy network on the
following scenario starting from the initial levels: 
$(B, 4)$, $(P, 0)$, $(C, 0)$, $(G,0)$, see Figure~\ref{fig:diagram}:



\begin{figure}[t]
\centering
\begin{tikzpicture}[>=latex',xscale=.8, yscale=.5]

\draw[draw=none,fill=blue!10] (-1,1) rectangle (11,2) ; 
\draw[draw=none,fill=blue!10] (-1,3) rectangle (11,4) ; 
\draw[draw=none,fill=blue!10] (-1,5) rectangle (11,6) ; 
\draw[draw=none,fill=blue!10] (-1,7) rectangle (11,8) ; 
\draw[draw=none,fill=blue!10] (-1,9) rectangle (11,10) ; 

\node at (-1,1) (p0) {};
\node[left] at (p0.west) {$0$};
\node at (-1,2) (p1) {};
\node[left] at (p1.west) {$1$};
\node at (-1,3) (c0) {};
\node[left] at (c0.west) {$0$};
\node at (-1,4) (c1) {};
\node[left] at (c1.west) {$1$};
\node at (-1,5) (g0) {};
\node[left] at (g0.west) {$0$};
\node at (-1,6) (g1) {};
\node[left] at (g1.west) {$1$};
\node at (-1,7) (b0) {};
\node[left] at (b0.west) {$0$};
\node at (-1,8) (b1) {};
\node[left] at (b1.west) {$1$};
\node at (-1,9) (b2) {};
\node[left] at (b2.west) {$2$};
\node at (-1,10) (b3) {};
\node[left] at (b3.west) {$3$};

\node[label=left:{$B=\left[ \phantom{\begin{array}{l} a\\ a\\ a\\ a \end{array}} \right.$}] at (-1,8.5) (b) {};
\node[label=left:{$G=\left[ \phantom{\begin{array}{l} a\\ a \end{array}} \right.$}] at (-1,5.5) (g) {};
\node[label=left:{$C=\left[ \phantom{\begin{array}{l} a\\ a \end{array}} \right.$}] at (-1,3.5) (c) {};
\node[label=left:{$P=\left[ \phantom{\begin{array}{l} a\\ a \end{array}} \right.$}] at (-1,1.5) (p) {};

%\draw[->] (p0) -- (p1) ;
%\draw[->] (c0) -- (c1) ;
%\draw[->] (g0) -- (g1) ;
%\draw[->] (b0) -- (b3) ;

%points horizontaux
\node at (-2,0) (t0) {};
\node[rectangle,draw,fill=blue,scale=.3,label=below:0] at (0,0) (t1) {};
\node[rectangle,draw,fill=blue,scale=.3,label=below:1] at (2,0) (t2) {};
\node[rectangle,draw,fill=blue,scale=.3,label=below:2] at (4,0) (t3) {};
\node[rectangle,draw,fill=blue,scale=.3,label=below:3] at (6,0) (t4) {};
\node[rectangle,draw,fill=blue,scale=.3,label=below:4] at (8,0) (t5) {};
\node[rectangle,draw,fill=blue,scale=.3,label=below:5] at (10,0) (t6) {};
\node[label=below:$time$] at (11,0) (t7) {};

% points verticaux
\node[rectangle,draw,fill=blue,scale=.3] at (-1,1) (k1) {};
\node[rectangle,draw,fill=blue,scale=.3] at (-1,2) (k2) {};
\node[rectangle,draw,fill=blue,scale=.3] at (-1,3) (k3) {};
\node[rectangle,draw,fill=blue,scale=.3] at (-1,4) (k4) {};
\node[rectangle,draw,fill=blue,scale=.3] at (-1,5) (k5) {};
\node[rectangle,draw,fill=blue,scale=.3] at (-1,6) (k6) {};
\node[rectangle,draw,fill=blue,scale=.3] at (-1,7) (k7) {};
\node[rectangle,draw,fill=blue,scale=.3] at (-1,8) (k8) {};
\node[rectangle,draw,fill=blue,scale=.3] at (-1,9) (k9) {};
\node[rectangle,draw,fill=blue,scale=.3] at (-1,10) (k10) {};

\draw[->] (t0) -- (t7) ; %axe du temps
\draw[->] (-1,0) -- (-1,11.5) ; %axe vertical

\path[draw,thick] (0,1) --(6,1) --node[midway,above,sloped]{$\alpha_1$} (6,2) -- (9,2) ;
\node[right] at (9,2) {$\cdots$};
\path[draw,thick] (0,3)  --node[midway,above,sloped]{$\alpha_3$} (0,4) -- (9,4) ;
\node[right] at (9,4) {$\cdots$};
\path[draw,thick] (0,5) --node[midway,above, sloped]{$\alpha_5$}  (0,6) -- (9,6) ;
\node[right] at (9,6) {$\cdots$};
\path[draw,thick] (0,10) -- (6,10) -- (6,7) -- (8,7) -- (8,9) -- (9,9) ;
\node[right] at (9,9) {$\cdots$};
\node[above] at (6,10) {$\beta_2,\beta_3,decay$};
\node[above] at (8,9) {$\beta_1$};

\end{tikzpicture}
\caption{Entities levels evolving with time corresponding to the scenario of Example~\ref{ex:intuitive_scenario}.}
\label{fig:diagram}
\end{figure}

      \begin{enumerate}

      \item Activate the GPS ($\alpha_5: \activ{(G,0)}{(G,1)}{0}{(G,+1)}$)

      \item Start a phone call ($\alpha_3: \activ{(C,0)}{(C,1)}{0}{(C,+1)}$)

      \item Three time units pass by -- no decay or \obligatory activities are involved

      \item One time unit passes by -- battery decays and enabled \obligatory
            activities\\
            %
            $\beta_2: \activ{(C,1)}{\emptyset}{3}{(B,-1)}$ and
            $\beta_3: \activ{(G,1)}{\emptyset}{3}{(B,-2)}$
            %
            are performed

      \item Plug the phone ($\alpha_1: \activ{(P,0)}{(P,1)}{0}{(P,+1)}$)

      \item One time unit passes by -- no decay but enabled
        \obligatory activity
        $\beta_1:\activ{(P,1)}{\emptyset}{1}{(B,+1)}$ is executed \hfill $\diamond$

      \end{enumerate}
      
\end{example}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\section{Petri Net Model}\label{sec:petri} 

In this section, we formalize \andy networks in terms
of high-level Petri nets. 
%
%We first formalize the notion of state of a
%network and then we specify the behavior of the network as the
%evolution of a high-level Petri net.
%In our approach, the model of time of an \andy network is managed
%explicitly in the functioning of the Petri net. 
%and not as the time
%evolution of the Petri net itself. This approach is relevant but makes
%uneasy to assess the temporal properties of the \andy framework because
%two \andy networks will give raise to two different Petri nets.
%% Cinzia: FALSE!
%%
%For this reason, we have developed an equivalent semantics in terms of
%timed automata. This semantics is presented in the next section.
We recall here their general notations together with some elements of their
semantics  \cite{DBLP:series/eatcs/Jensen92}.

\begin{definition}[High-level Petri nets]\label{def:PTS} 
A \emph{high-level Petri net}  is a tuple $(P, T, F, L, M_0)$ where:
\begin{itemize}
 \item $P$ is the set of places, $T$ is the set of transitions, with $P \cap T = \emptyset$;

 \item $F \subseteq (P \times T) \cup (T \times P)$ is the set of arcs; 
 \item $L$ is the labeling  of $P \cup T\cup F$%places $P$, transitions $T$ and arcs $F$   to  a set of labels 
defined as follows:
\renewcommand{\labelitemii}{$-$} 
\begin{itemize}
 \item $\forall p \in P$, $L(p) $ is a set of values;% the type of $p$;%, \ie a (possibly infinite) set or Cartesian product of sets of integer values;
 \item $\forall t \in T$, $L(t)$ is a  computable boolean expression (a guard);%  with variables and integer values; 
 \item and $\forall f\in F$, $L(f)$  is a  tuple of variables or values.% compatible with the adjacent place.  
\end{itemize}
 \item $M_0$ is the initial marking putting a multiset of tokens in $L(p)$ in each   $p \in P$.\looseness=-1
\end{itemize} 
\end{definition}
Observe that we are considering a subclass of high-level Petri nets where at most one arc per direction  for each pair place/transition   is allowed and only one token can flow through. 
The behavior of high-level Petri nets is defined as usual: markings are functions from places in $P$ to multisets of possibly structured tokens in $L(p)$ and a transition $t \in T$ is \emph{enabled} at  marking $M$, if there exists a valuation $\sigma$ of all variables in the labeling of $t$  such that the guard $L(t)$ evaluates to true ($L_{\sigma}(t) = \mathsf{true}$) and there are enough tokens in all input places $p$ to satisfy the corresponding input arcs, \ie $L_{\sigma}((p,t)) \in M(p)$.
% and all input arc labels are $ \qquad \forall q \in \pre{t},   [L((q,t))]_{\sigma} \in M(q),$$
%where $\pre{t} =\{q\in Q \mid (q,t) \in F\}$ denotes the set of input places of a transition $t$. 
Then, the firing of $t$ produces the marking $M'$:  
$$\forall p \in P, M'(p) = M(p) - L_{\sigma}((p,t)) + L_{\sigma}((t,p)). $$
with $L_{\sigma}(f) = 0 $ if $f\notin F$, $-$ and $ +$ are  multiset  operators for removal and adding of one element, respectively. We denote it by $\firing{M}{t}{\sigma}{M'}$. 

As usual, in figures, places are represented as rounds, transitions as squares, 
and arcs as directed arrows.
By convention, primed version of variables (\eg $x'$) are used to annotate 
output arcs of transitions, their evaluation is  
possibly computed using unprimed 
variables (\eg $x$) appearing on input arcs. 
With an abuse of notation, singleton markings are denoted without brackets, 
the same is used in  arc annotations. 
Also we refer to valuated variables without effectively mentioning the valuation $\sigma$: \ie we say that the current value of variable $w$ is $w$ instead of $\sigma(w)$.
An example of firing is shown in  
Appendix \ref{app:exfiring}. 
We say that a marking $M$ is \emph{reachable} from the initial marking 
$M_0$ if there exists a firing sequence $(t_1, \sigma_1), \mydots, (t_n, \sigma_n)$ such that 
 $\firing{M_0}{t_1}{\sigma_1}{M_1} \mydots \firing{M_{n-1}}{t_n}{\sigma_n}{M}$.







\paragraph{\bf Formalization of \andy.}


Each entity $\entity \in \entities$ is modeled by a single place $p_{\entity}$. A token in $p_{\entity}$ is a tuple
$\tuple{\bool_\entity, \refr_\entity, \birth_\entity}$ where
%%
$\bool_\entity$ is  the current level of $\entity$; 
%%
$\refr_\entity$ is a counter storing the duration spent in the current level since the last update: $0 \leq \refr_\entity \leq \life_\entity(\bool_\entity)$; 
%%
and $\birth_\entity$ is a tuple of counters with $\setlev_\entity$ fields (one for
each level).  Each counter $\birth_{\entity}[i]$ contains a
duration interpreted as follows:
$$
\birth_{\entity}[i] = 
\begin{cases}
\begin{minipage}{5.2cm}
  since how long $\entity$ has reached level  $i$
\end{minipage}
 &  \text{for }  0 \leq i \leq \lev_{\entity}\\
\\
\begin{minipage}{5.2cm}
   since how long $\entity$ has left level $i$ \\(or $0$ if $\entity$ has not yet reached $i$).
\end{minipage} 
& \text{for } \lev_{\entity} < i \leq \setlev_{\entity}-1              
\end{cases}
$$

Each place is initialized to $\tuple{\level{\entity}, 0,
  0^{\setlev_\entity} }$ where $\level{\entity}$ is the given initial
level of $\entity$ and $0^{\setlev_\entity}$ denotes vector $\birth_\entity$ of counters
uniformly initialized with zero.
 

\begin{newnotation}
      We denote
      by $\birth\sub{x}{[l \mydots l + n ]}$ the systematic update of
      values in counters $\birth[l] \mydots \birth[l+n]$ to $x$. 
      $\inc{D}{\birth}$ is the increment by one of all values in $\birth$:
      \ie $\forall k \in [0 \mydots \setlev_\entity-1]$, $\birth[k] =
      \min(\birth[k]+1, D)$ with $D \in \nat$.
\end{newnotation}

In order to cope with time aspects present in \andy, we introduce a tick transition $t_c$ (Figure \ref{fig:clock}) that represents the time progression.  Its effect is the one described in Phase Ph. \ref{item:clock} above: it increments  counters of entities,  takes care of the decay and simultaneously performs all enabled \obligatory activities. More precisely updates due to time progression  are performed as follows:
      \begin{description}
      \item [Time: ] All counters in the entities are incremented by
            one: we pass from $\tuple{\lev, \refr, \birth}$ to
            $\tuple{\lev, \refr+1, \inc{D}{\birth}}$.  We assume that
            counter $\refr$ remains unchanged for levels of unbounded
            duration, and once a value in $\birth$ has reached $D$ (the maximal duration of activities) it is
            useless to increment it, as for all values greater than $D$, the guard of all activities involving the entity is satisfied.  

      \item [Decay: ]An entity may stay at level $\lev$ for
            $\life(\lev)$ time units (\ie $\refr \leq \life(\lev)$).
            Decay happens as soon as the interval $\life(\lev)$ is
            elapsed and is obtained by decreasing the level by one, till
            reaching level zero.  More formally, we pass from
            $\tuple{\lev, \refr, \birth}$ to $\tuple{\lev - 1, 0,
              \inc{D}{\birth}\sub{0}{\lev}}$.

      \end{description}

Updates on a place $p_r$ of a result entity $r$ at level $\lev_r$ containing token  $\tuple{\lev_r, \refr_r, \birth_r}$, due to an activity $\rho$ (\ie $(r,\pm n) \in R_{\rho}$ with $n\in \nat$) 
are performed\footnote{For the sake of simplicity, in the explanation we consider updates that do not exceed allowed boundaries, these cases are handled as expected in Definition \ref{def:rs}.} as follows : 
\begin{description}
 \item[Increase $+n$:]  
   $\tuple{\lev_r + n, 0, \birth_r\sub{0}{[\lev_r + 1\mydots \lev_r + n]}}$.
  $\lev_r$ becomes $\lev_r +n$, $\refr_r$ is reset to 0 restarting the counter  for level $\lev_r +n$ and 
$\birth_r$ is updated to record the change to the new level by resetting the counters $\birth_r[i]$ for all levels $i$ from $\lev_r + 1$ to $\lev_r + n$.
 
 \item[Maintenance $0$:]  $\tuple{\lev_r, 0, \birth_r}$: the current level is recharged resetting $\refr_r$ to 0.

  \item[Decrease $-n$:]  
	    $\tuple{\lev_r - n, 0, \birth_r\sub{0}{[\lev_r-n+1 \mydots \lev_r] }}$. This case is symmetric to the increase one, except for the treatment of $\birth_r$ that is updated by resetting  counters   $\birth_r[i]$
for all levels $i$  from  $\lev_r - n + 1$ to $\lev_r$.
\end{description}
%%
%%
% Once performed, the next execution of the same activity is possible after at least $\dur{\rho}$ time units.






Finally, every \potential activity $\alpha \in \Reac$ is modeled with  a transition $t_{\alpha}$ (Figure \ref{fig:reaction})  %with a special place $p_{\alpha}$ that  ensures that the same activity is not executed more than once every $\dur{\alpha}$ time units, 
complying to Phase Ph. \ref{item:reaction} above.


%%%%
%%%% CE QUE JE N'AI PAS UTILISE DANS LA SECTION PRECEDENTE
%%%%



%% $\birth_\entity$ is a tuple with $|\setlev_\entity|$ fields (one for
%% each level) 
%%  each $\birth[j]$ containing the length of time interval from
%% 0 to a constant $D$ where $D = \max\{\dur{\rho} \mid \rho \in \Syn \cup
%% \Reac\}$.








It is also worth observing that if an entity is continuously sustained
by some activities then it remains available in the system at a certain
level for a period that could be longer than the corresponding decay
time. This is witnessed by the fact that the values of counters
$\birth[\lev]$ and $\refr$ can be different: the first representing the
availability at level $\lev$ and the second the duration since last
update.


\begin{example}[Mobile phone battery - Execution scenario]
\label{ex:formal_scenario}
The evolution of tuples of counters $\birth{}$ is illustrated for the 
scenario from Example~\ref{ex:intuitive_scenario} starting from 
the initial state. We have the following sequence of markings:
$$
\begin{array}{ccccc}
 & p_B &p_P&p_C&p_G\\
\mathit{init} & \quad \tuple{4, 0, [0,0,0,0,0]} \quad 
 & \quad \tuple{0, 0, [0,0]} \quad 
 &\quad  \tuple{0, 0, [0,0]}\quad 
 &\quad  \tuple{0, 0, [0,0]}\quad \\
%we activate the GPS ($\alpha_5: \activ{(G,0)}{(G,1)}{0}{(G,+1)}$)
1 & \quad \tuple{4, 0, [0,0,0,0,0]}\quad
 &\quad \tuple{0, 0, [0,0]}\quad
&\quad \tuple{0, 0, [0,0]}\quad
 &\quad \tuple{1, 0, [0,0]}\quad \\
%start a phone call ($\alpha_3: \activ{(C,0)}{(C,1)}{0}{(C,+1)}$)
2 & \quad \tuple{4, 0, [0,0,0,0,0]} \quad
& \quad \tuple{0, 0, [0,0]} \quad
 &\quad \tuple{1, 0, [0,0]}\quad
 &\quad \tuple{1, 0, [0,0]}\quad \\
%3 time units pass by (no decay or obligatory activity involved)
3 & \quad
 \tuple{4, 3, [3,3,3,3,3]} \quad
& \quad \tuple{0, 0, [3,3]} \quad
& \quad \tuple{1, 0, [3,3]} \quad
& \quad \tuple{1, 0, [3,3]}\quad \\
% 1 time unit pass by, battery decays, and enabled obligatory activities\\ $\beta_2: \activ{(C,1)}{\emptyset}{3}{(B,-1)}, \beta_3: \activ{(G,1)}{\emptyset}{3}{(B,-2)}$ are performed
4 & \quad
 \tuple{0, 0, [0,0,0,0,0]} \quad
& \quad \tuple{0, 0, [3,3]}\quad
& \quad \tuple{1, 0, [3,3]}\quad
& \quad \tuple{1, 3, [3,3]}\quad \\
%we plug the phone ($\alpha_1:  \activ{(P,0)}{(P,1)}{0}{(P,+1)}$)
5 & \quad
 \tuple{0, 0, [0,0,0,0,0]} \quad
& \quad \tuple{1, 0, [3,0]} \quad
& \quad \tuple{1, 0, [3,3]} \quad
& \quad \tuple{1, 0, [3,3]} \quad \\
% 1 time unit passes by with no decays and enabled obligatory activity\\
%\beta_1:\activ{(P,1)}{\emptyset}{1}{(B,+1)}$ is executed
6 & \quad
 \tuple{1, 0, [1,0,1,1,1]} \quad
 &\quad \tuple{1, 0, [3,1]} \quad
 &\quad \tuple{1, 0, [3,3]} \quad
 &\quad \tuple{1, 0, [3,3]} \hfill \diamond
\end{array}
$$

\end{example}


%\subsection{\bf Petri net modeling of \andy}


\begin{figure}[t]
\centering
\subfigure[Clock transition. \label{fig:clock}]{
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=20,auto]

  \node [place, label = right: $p_{\alpha}$, label = above: $\vdots$,label = below: $\vdots$] at (3.5,0) (Pc){};
  \node [place, label=left:$p_{\entity}$,label = above: $\vdots$,label = below: $\vdots$]at (0,0)  (R){};

  \node [transition] (tC) at (2,0) {$t_{c}$}
   edge [pre,bend left]    node[above] {$w_{\alpha}$}    (Pc)
   edge [post,bend right]   node[below]{$w'_{\alpha}$}    (Pc)
   edge [pre,bend right]    node[above] {${\scriptstyle \tuple{\bool_{\entity},\refr_{\entity},\birth_{\entity}}}$}    (R)
   edge [post,bend left]    node[auto] {${\scriptstyle \tuple{\bool_{\entity}',\refr_{\entity}',\birth_{\entity}'}}$}    (R);
  
\end{tikzpicture}
} \quad
\subfigure[Transition for $\alpha\in\Reac$. \label{fig:reaction}]{
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=20,auto]

 \node [place, label = right: $p_r$,label = left: $\cdots$] at (0,-1.5) (P){};
 %\node [place, label = above: $\Pclock$] at (0,2) (Pc){};
 \node [place, label = below: $p_a$,label = above: $\vdots$] at (-2,0) (R){};
 \node [place, label = below: $p_i$,label = above: $\vdots$] at (2,0) (I){};
 \node [place, label = right: $p_{\alpha}$] at (0,1.5) (qw){};
 
 \node [transition] at (0,0) (tr) {$t_{\alpha}$}
  % edge [pre and post]    node[above] {$z$}    (Pc)
   edge [pre and post]    node[above] {${\scriptstyle \tuple{\bool_{\entity},\refr_{\entity},\birth_{\entity}}}$}   (R)
   edge [pre and post]    node[above] {${\scriptstyle \tuple{\bool_{\entity},\refr_{\entity},\birth_{\entity}}}$}     (I)
   edge [pre, bend right]    node[left] {${\scriptstyle \tuple{\bool_{\entity},\refr_{\entity},\birth_{\entity}}}$}   (P)
   edge [post, bend left]   node[right] {${\scriptstyle \tuple{\lev'_r,\refr'_r,\birth_r'}}$}     (P)
   edge [pre, bend left]    node[left] {$w_{\alpha}$}   (qw)
   edge [post, bend right]   node[right] {$w'_{\alpha}$}     (qw);
   
  
\end{tikzpicture}
}
\caption{Scheme of Petri net modeling of \andy.}
\end{figure}



\begin{definition}[\rsd network]\label{def:rs}
 Given an  \andy network $(\entities, \Syn, \Reac)$ with initial 
state $(\entity, \level{\entity})$ for each $\entity \in \entities$, 
%Let $D = \max\{\dur{\alpha} \mid \alpha \in \Syn \cup \Reac\}$. 
the high-level Petri net representation is defined as 
tuple $(P, T, F, L, M_0)$ where  $\lev$, $\lev'$, $\refr$, $\refr'$, $\birth$, 
$\birth'$, $w$, $w'$ range over variables and:
\begin{itemize} 
 \item $P = \{p_\entity \mid  \entity\in{\entities}\} \cup \{p_{\rho} \mid  \rho \in \Syn \cup \Reac \}; $
 \item $T= \{t_c \} \cup \{t_{\alpha} \mid \alpha \in \Reac \}$;

 \item $F= \{(p,t_c),(t_c, p) \mid p \in P \} \quad  \cup$ \\
 \hspace*{0.63cm} $ \{ (p_\entity,t_{\alpha}),(t_{\alpha}, p_\entity), (p_{\alpha},t_{\alpha}),
		(t_{\alpha}, p_{\alpha}) \mid \alpha \in \Reac, 
		\entity \in A_{\alpha} \cup I_{\alpha} \cup R_{\alpha} \}$

 \item Labels for places in $P$: 
\[
\begin{array}{c}
  L(p_{\rho})  = [0 \mydots D]  \text{ for each } \rho \in \Syn \cup \Reac  \\
L(p_\entity) = [0\mydots\setlev_\entity-1] \times [0 \mydots d] \times  [0 \mydots D]^{\setlev_\entity}  
\text{ for each } \entity\in\entities 
\end{array}
\]
with $d = \max\{\life_{\entity}(i)\mid i \in [0 \mydots \setlev_\entity-1]\}$ and $D = \max\{\dur{\rho}\mid \rho \in \Syn \cup \Reac\}$
\item Labels for arcs in $F$:
\[
\begin{array}{llr}
 L((p_{\rho}, t_c)) = w_{\rho} & L((t_c, p_{\rho} )) = w'_{\rho}\\
    L((p_\entity, t_c)) = \tuple{\bool_\entity, \refr_\entity, \birth_\entity} 
		& L((t_c, p_\entity)) = \tuple{\bool_\entity', \refr_\entity', \birth_\entity'} 
		& \text{ for each } \entity\in\entities
\end{array}
\]
For each \potential activity $\alpha\in\Reac$ and $\entity \in A_{\alpha} \cup I_{\alpha} \cup R_{\alpha}$:
\[
\begin{array}{llr}
      L((p_\entity, t_{\alpha})) = \tuple{\bool_\entity, \refr_\entity, \birth_\entity} \quad 
		& L((t_{\alpha}, p_\entity)) = \begin{cases}
                           \tuple{\bool_\entity, \refr_\entity, \birth_\entity} & \text{if } \entity\notin R_{\alpha}\\
                           \tuple{\bool_\entity', \refr_\entity', \birth_\entity'} & \text{otherwise}
                          \end{cases}\\

     L((p_{\alpha}, t_{\alpha})) = w_{\alpha} & L((t_{\alpha}, p_{\alpha} )) = w'_{\alpha}
\end{array}
\]

\input{algorithm}

% \begin{figure}[t]
% \[
% \begin{array}{l}
% \text{Algorithm } \mathit{Calc}\\
% \quad \text{\bf for each } \rho \in \Syn \cup \Reac \text{ {\bf do} } w_{\rho}'=\max(w_{\rho}+1,D)\\
% %\text{endfor}\\
% 
% \quad\text{\bf for each } \entity\in\entities \text{ {\bf do}}\\
% \quad\qquad \lev_\entity'=\lev_\entity 
% \quad\qquad \refr_\entity'=\refr_\entity
% \quad\qquad \birth_\entity'=\inc{D}{\birth_\entity}\\
% \quad\qquad
% \begin{array}{@{}lll}
% \text{{\bf if }} & \life(\lev_\entity) \neq \omega &\text{  {\bf then} } \quad \refr_\entity'= \refr_\entity + 1\\
% \text{{\bf if }} & \refr_\entity > \life(\lev_\entity) &\text{  {\bf then} } \quad \lev_\entity'= \max(0, \lev_\entity -1) \quad\quad  \refr_\entity'= 0
% \end{array}\\
% %\text{endfor}\\
% 
% \quad\text{{\bf for each} } \beta \in \Syn \text{ {\bf do}}\\
% \quad\qquad \text{{\bf if} } \bigwedge_{(a, \level{a}) \in A_{\beta}}(\lev_a \geq \level{a} \wedge  \birth[\level{a}] \geq \dur{\beta} )  \quad \wedge\\
% \quad\qquad \quad \bigwedge_{(i, \level{i}) \in I_{\beta}}(\lev_i < \level{i} \wedge \birth[\level{i}] \geq \dur{\beta} )  \quad \wedge 
%  \quad\quad (w_{\beta} \geq \dur{\beta}  )\\
% \quad\qquad\text{{\bf then} }
%  \quad\qquad \qquad w'_{\beta} = 0\\
%  \quad\qquad \qquad \text{{\bf for each} } (r,v)\in R_{\beta} \text{ {\bf do}} \\
%  \quad\qquad \qquad \qquad \lev_r'= \lev_r' +v \qquad \refr_r'= 0\\
% %\qquad \qquad \text{endfor} \\
% %\qquad \text{endif}\\
% 
% \quad\text{{\bf for each} } \entity \in \entities \text{ {\bf do}}\\ %Est-ce bien ça ? no c'etait un typo
% \quad\qquad \lev_r'= \max(0, \min(\lev_r', \setlev_r-1 ) \\
% \quad\qquad \text{{\bf case} } \lev_\entity' - \lev_\entity \text{ {\bf of}}\\
% \quad\qquad \qquad [\lev_\entity' - \lev_\entity<0]:  \birth_\entity'=\birth'_\entity\sub{0}{[\lev_\entity'+1\mydots \lev_\entity]}\\
% \quad\qquad \qquad [\lev_\entity' - \lev_\entity>0]:  \birth_\entity'=\birth_\entity'\sub{0}{[ \lev_\entity+1 \mydots \lev_\entity']}\\
% %\qquad \text{endcase}\\
% 
% 
% %\text{endfor}\\
% \quad\text{{\bf return} } \bigwedge_j x'_j=c_j \\
% \end{array}
% \]
% where $x_j'$ is the variable labeling  an output arc of $t_c$ and $c_j$ is its evaluation via $\mathit{Calc}$ 
% 
% \caption{$\mathit{Calc}$ algorithm} \label{fig:calc}
% \end{figure}



\item Labels for transitions in $T$:
 \[
 L(t_c) = \mathit{Calc}
 \]
where $\mathit{Calc}$ is the  algorithm in Algorithm \ref{fig:calc} whose input is the unique valuation $\sigma$ for net variables of input arcs of $t_c$ coming from the current marking,  and which returns the conjunction of equalities of the form $\mathtt{var'} = \mathtt{const}$ for each net variable $\mathtt{var'}$ labeling an output arc  of $t_c$ and  $\sigma(\mathtt{var'})=\mathtt{const}$.
 
For each activity $\alpha\in\Reac$:
\[
\begin{array}{lcl}
L(t_{\alpha}) \! &=&  w_{\alpha} \geq \dur{\alpha}  \wedge  w'_{\alpha} = 0 \quad \wedge \\
&& \bigwedge_{(a, \level{a}) \in A_{\alpha}}(\lev_a \geq \level{a} \wedge \birth[\level{a}] \geq \dur{\alpha} )  \quad \wedge\\
&&  \bigwedge_{(i, \level{i}) \in I_{\alpha}}(\lev_i < \level{i} \wedge \birth[\level{i}] \geq \dur{\alpha} )  \quad  \wedge \\


&& \bigwedge_{(r,+n) \in R_{\alpha}} C_{r+} \wedge \bigwedge_{(r,0) \in E_{\alpha}}C_{r0} \wedge  \bigwedge_{(r,-n) \in R_{\alpha}}C_{r-},\\  
\end{array}
\]
with
\[
\begin{array}{ll}
C_{r+} \!&:\!  \tuple{\lev'_r, \refr'_r, \birth'_r} = \tuple{\min(\lev_r +n, \setlev_r-1), 0, \birth_r\sub{0}{[\lev_r +1 \mydots \min(\lev_r +n, \setlev_r-1 ]}} \\
C_{r0} \!&: \! \tuple{\lev'_r, \refr'_r, \birth'_r} = \tuple{\lev_r, 0, \birth_r} \\

C_{r-} \!&: \! \tuple{\lev'_r, \refr'_r, \birth'_r} = \tuple{\max(0,\lev_r-n), 0, \birth_r\sub{0}{[\min(0,\lev_r-n) \mydots \lev_r]}}.
\end{array}
\]

 

\item For each $p\in P$, $\entity\in \entities$ and $\alpha\in \Reac$, the initial marking $M_0$ is:
\[
M_0(p) =
\begin{cases}
 0 & \text{if } p = p_{\rho} \\
 \tuple{\level{s},0,0^{\setlev_\entity}}& \text{if } p = p_\entity
\end{cases}
\]
\end{itemize}
\end{definition}



We now comment on the transitions guards. 
Input and output arcs between the same place and transition with the same label (read arcs) are denoted in figures with a double-pointed arrow with a single label.
 We detail the conditions and the results of firing of $t_{\alpha}$ corresponding to a \potential activity $\alpha= \activ{A}{I}{\dur{}}{R}$. We have:
\begin{itemize}
 \item each activator $a \in A$ has to be present at least at  level $\level{a}$ for at least $\dur{}$ time units, this is expressed by  guard $\lev_a \geq \level{a} \wedge \birth[\level{a}] \geq \dur{} $; 
 \item each inhibitor $i\in I$ has not to exceed  level $\level{i}$ for at least $\dur{}$ time units,  this is guaranteed by guard 
$\lev_i < \level{i} \wedge \birth[\level{i}] \geq \dur{}$;
\item each result is updated according to conditions $C_{r+}$ (increase), $C_{r0}$ (maintenance), $C_{r-}$ (decrease);
\item place $p_{\alpha}$ retains whether the activity can been performed $w_{\alpha}\geq\dur{}$.

%
%if a result $r \in R $ has to be increased maintained or decreased then the corresponding place $p_r$ is updated to:
%\begin{description}
 %\item [increase:] $\tuple{\min(\lev_r +n, \setlev_r-1), 0, \birth_r\sub{0}{[\lev_r +1 .. \min(\lev_r +n, \setlev_r-1 ]}}$
 %\item [maintenance:] $ \tuple{\lev'_r, \refr'_r, \birth'_r} = \tuple{\lev_r, 0, \birth_r} $
 %\item [decrease:] $ \tuple{\lev'_r, \refr'_r, \birth'_r} = \tuple{\max(0,\lev_r-n), 0, \birth_r\sub{0}{[\min(0,\lev_r-n).. \lev_r]}}$. 
%\end{description}
\end{itemize}
Firing of transition $t_c$ is always enabled and all connected places are modified according to algorithm $\mathit{Calc}$, which updates the level of all entities dependently if they are involved in a \obligatory activity or decay and increments the length of time interval in $p_{\rho}$ ($w'_{\rho} = w_{\rho}+1$) for all $\rho \in \Syn \cup \Reac$ unless a \obligatory activity $\beta$ is performed in which case the corresponding $w_{\beta}$ is set to 0.






%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Encoding into Timed Automata} \label{sec:timedauto}


In this section, we give a semantics of \andy network in terms of timed
automata. This semantics is not straightforward because the management
of the \obligatory rules may lead to the activation of an arbitrary
subset of $\Reac$, and the summation of the corresponding increment. We
will show that it can be achieved at the price of a translation
 exponential in the number of activities. 

Despite this difficulty, providing a semantics in terms of timed
automata \cite{DBLP:journals/tcs/AlurD94} is appealing: since their introduction 
 they have been widely used to
model complex real time systems and to check their temporal
properties. Since then many variants have been considered depending of
synchronization policies (synchronous, urgent, broadcast \cite{uppaal}).


The main result of this section is that the semantics in term of timed
automata is equivalent to the semantics in terms of high-level Petri
net.



\paragraph{\bf Timed automata.}

A timed automaton is an annotated directed (and connected) graph, 
with an initial node and provided with a finite set of non-negative real 
variables called \emph{clocks}. 
Nodes (called \emph{locations}) are annotated with \emph{invariants} 
(predicates allowing to enter or stay in a location).
Arcs are annotated with \emph{guards}, 
\emph{communication labels}, and possibly with some clock \emph{resets}. 
Guards are conjunctions of elementary predicates of the form  
$x~\op~c$, where $\op\in\{>,\geq,=,>,\leq\}$ where $x$ is a clock and 
$c$ a (possibly parameterized) positive integer constant.
As usual, the empty conjunction is interpreted as true. 
The set of all guards and invariant predicates will be denoted by $G$. 

%In figures, locations will be represented by round nodes, the initial one having a double boundary. 

\begin{definition}\label{def:ta} A \emph{timed automaton} $\TA$
is a tuple $(L,l^0,X,\Sigma,\arcs,\inv)$, where 
\begin{itemize}
	\item $L$  is a set of locations with $l^0\in L$ the initial one, $X$ is the set of clocks, 
	\item $\Sigma=\Sigma^s\cup\Sigma^u\cup\Sigma^b$ is a set of communication labels, 
	where $\Sigma^s$ are synchronous, $\Sigma^u$ are synchronous and urgent, 
	and $\Sigma^b$ are broadcast ones,
	\item $\arcs \subseteq L \times (G \cup \Sigma \cup R) \times L$ 
is a set of arcs between locations with a guard in $G$, 
a communication label in $\Sigma\cup\{\epsilon\}$, and a set of clock resets in $R=2^X$;
for all $a\in\Sigma^u$, we require the guard to be $\true$; 
  \item $\inv: L \rightarrow G$ assigns invariants to locations. 
\end{itemize}
\end{definition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

It is possible to define a synchronized product of a set of timed automata 
that work and synchronize in parallel. 
The automata are required to have disjoint sets of locations, but
may share clocks and communication labels which are used for synchronization. 
We define three communication policies: 
\begin{itemize}
	\item \emph{synchronous} communications through
		labels $a\in\Sigma^s$ that require all the automata having label $a$  
		to synchronize on $a$; 
	\item \emph{synchronous urgent} communications through 
		labels $u\in\Sigma^u$ that are synchronous as above but \emph{urgent} meaning that
		there will be no delay if transition with label $u$ can be taken;
  \item \emph{broadcast} communications through labels $b!,b?\in\Sigma^b$ meaning that
	a set of automata can synchronize if one is emitting;
	notice that, a process can always emit (\eg $b!$) 
	and the receivers ($b?$) must synchronize if they can.
\end{itemize}

The synchronous product $\TA_1\parallel \ldots \parallel \TA_n$ 
of timed automata, where for each $j\in[1,\ldots,n]$, 
$\TA_j = (L_j, l^0_j,X_j,\Sigma_j,\arcs_j,\inv_j)$ and all $L_j$ are 
pairwise disjoint sets of locations is
the timed automaton $\TA=(L, l^0,X,\Sigma,\arcs,\inv)$ such that:
\begin{itemize}
\item $L=L_1\times\ldots\times L_n$ and $l^0=(l^0_1,\ldots,l^0_n)$, 
$X=\bigcup_{j=1}^n X_j$, $\Sigma=\bigcup_{j=1}^n \Sigma_j$,
\item $\forall l=(l_1, \ldots, l_n)\in L\colon \inv(l) = \bigwedge_j \inv_j(l_j)$,
\item $\arcs$ is the set of arcs 
$(l_1, \ldots, l_n) \stackrel{g,a,r}{\longrightarrow} (l'_1, \ldots, l'_n)$
such that (where for each $a\in\Sigma^s\cup\Sigma^u, 
S_a=\{j\mid 1\leq j \leq n, a\in \Sigma^s_j\cup\Sigma^u_j\}$):
	for all $1\leq j \leq n$, if $j\not\in S_a$, then $l_j'=l_j$, otherwise
	there exist $g_j$ and $r_j$ such that 
	$l_j \stackrel{g_j,a,r_j}{\longrightarrow} l_j'\in E_j$; $g=\bigwedge_{j\in S_a} g_j$
	and $r=\bigcup_{j\in S_a} r_j$.
\end{itemize}

The semantics of a synchronous product $\TA_1\parallel \ldots \parallel \TA_n$
is that of the underlying timed automaton $\TA$
(synchronizing on synchronous and broadcast communication labels) as recalled below, 
with the following notations. 
A location is a vector $l = (l_1, \ldots, l_n)$. 
We write $l[l'_j/l_j, j\in S]$ to denote the location $l$ in which the 
$j$th element $l_j$ is replaced by $l'_j$, for all $j$ in some set $S$.
A valuation is a function $\nu$ from the set of clocks to the non-negative reals. 
Let $\mathbb{V}$ be the set of all clock valuations, and $\nu_0(x) = 0$ 
for all $x \in X$.  
We shall denote by $\nu\vDash F$ the fact that the valuation $\nu$ 
satisfies (makes true) the formula $F$.
If $r$ is a clock reset, we shall denote by $\nu[r]$ 
the valuation obtained after applying clock reset $r\subseteq X$ to $\nu$; 
and if $d\in\mathbb{R}_{> 0}$ is a delay, 
$\nu+d$ is the valuation such that, for any clock $x\in X$, 
$(\nu+d)(x)=\nu(x)+d$.

The semantics of a synchronous product $\TA_1\parallel \ldots \parallel \TA_n$
is defined as a timed transition system $(S,s_0,\rightarrow)$,
where $S = (L_1 \times,\ldots\times L_n) \times \mathbb{V}$ is the set of states, 
$s_0 = (l^0, \nu_0)$ is the initial state, and 
$\rightarrow \subseteq S \times S$ is the transition relation defined by:
\begin{itemize}	
	%\item (silent): $(l,\nu) \rightarrow (l',\nu')$ 
	%if there exists $l_i \stackrel{g,~,r}{\longrightarrow} l'_i$, for some $i$, 
	%such that $l'=l[l'_i/l_i]$, $\nu\vDash g$ 
	%and $\nu'=\nu[r]$, 
	\item (sync): $(\bar{l},\nu) \rightarrow (\bar{l'},\nu')$ if 
	there exist arc $l \stackrel{g,a,r}{\longrightarrow} l'\in \arcs$ 
	such that $\nu\vDash g$, $\nu'=\nu[r]$,
	for $S_a=\{j\mid 1\leq j\leq n, a\in\Sigma^s_j\}$, 
	$l'=l[l'_j/l_j, j\in S_a]$, 
	and there is no enabled transition with urgent communication label
	from $(\bar{l},\nu)$;
	
	\item (urgent): as (sync) but $a\in\Sigma^u$ and there is no delay
	if transition with urgent communication label can be taken;
	 
	\item (broadcast): $(\bar{l},\nu) \rightarrow (\bar{l'},\nu')$ if
	there exist an output arc $l_j \stackrel{g_j,b!,r_j}{\longrightarrow} l_j'\in \arcs_j$ 
	and a (possibly empty) set of input arcs of the form
	$l_k \stackrel{g_k,b?,r_k}{\longrightarrow} l_k'\in \arcs_k$ such that 
	for all $k\in K=\{k_1,\ldots,k_m\}\subseteq\{l_1,\ldots,l_n\}\setminus\{l_j\}$,
	the size of $K$ is maximal, $\nu\vDash \bigwedge_{k\in K\cup\{j\}} g_k$,
	$l'=l[l'_k/l_k, k\in K\cup\{j\}]$ and $\nu'=\nu[r_k, k\in K\cup\{j\}]$;
	
	\item (timed): $(l,\nu)\rightarrow (l,\nu+d)$ if $\nu+d\vDash \inv(l)$. 
\end{itemize} 
An example of the behavior of timed automata can be found in Appendix \ref{app:ta}.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\paragraph{\bf Encoding into timed automata.}
We are now ready to introduce the encoding of the high-level Petri net formalization of $\andy$, to this aim we need to add some notation:

 \begin{newnotation}
Let $\Tag=\{\beta_1,\ldots,\beta_n\}$ be the set of all \obligatory activities identifiers from $\Syn$,
ordered alphabetically, \ie $\beta_i<\beta_j$ if $i<j$. 
We denote by 
\[
\Tag^{\circledast}=\{ seq(h) \mid h\in \mathcal{P}(\Tag) \wedge h\neq\emptyset \} \cup \{ \varepsilon\},
\] 
the set of sequences $seq(h)$ obtained by concatenating the identifiers in non-empty subsets $h$ of $\Tag$, where for each $h=\{\beta_{i_1},\ldots,\beta_{i_m}\mid \forall j,k:~ i_j<i_k \}\in \mathcal{P}(\Tag)$, $seq(h)=\beta_{i_1}\cdots \beta_{i_m}$. We assume that if $\Tag^{\circledast}=\{h_1 \mydots h_k\}$, then the $h_i$'s are ordered by decreasing length and alphabetically in such a way that $h_1=\beta_1\cdots\beta_{|\Tag|}$ and $h_k = \varepsilon$. 

Moreover, $\beta_i=h[i]$ is the identifier at the $i$-position, and  $h=h_1-h_2$ is  the sequence of identifier in $h_1$ without those in $h_2$.
  %Let $Lab$ be a set of labels, we denote with 
  %$$Lab^{\circledast} = \{x_1 \cdots x_n \mid n \in [1..|Lab|], \forall i,j \in [1..n], x_i \in Lab \wedge x_i < x_j  \} \cup \{ \varepsilon\}$$ 
  %the set of labels obtained by concatenating in alphabetical order ($<$) the labels in $Lab$, using them at most once.  
  %
  %Labels in $Lab^{\circledast} $ can be alphabetically ordered from the longest to $\varepsilon$ thus we denote  $Lab^{\circledast} = \{t_1 \mydots t_n \} $ where $t_1$ is the word composed of all labels in $Lab$ and $t_n = \varepsilon$. 
 \end{newnotation}

 The encoding of an $\andy$ Petri net is the synchronized product of one timed automaton for each entity in \entities  together with a set of auxiliary automata that are used to handle \potential and \obligatory activities.  
 The idea is that the global state of an \andy network is divided into its local counterparts represented by state of entities (\ie their levels). Thus for each entity $\entity$ we build a timed automaton $\TA(\entity, \level{\entity})$ which has as many locations as the levels in $\entity$. Auxiliary automata are used to implement the encoding of places $p_{\rho}$ ($\TA(\rho)$ for $\rho \in \Syn \cup \Reac$) and to realize time progression together with \obligatory activities ($\TA_{\tick}$). 
 More formally:
 
 \begin{definition} Given an \andy network $(\entities, \Syn, \Reac)$, with initial expression level $\level{\entity}$ for each $\entity \in \entities$, the corresponding timed automata encoding is 
 \[\enc{(\entities, \Syn, \Reac)} = \prod_{\entity \in \entities} \TA(\entity,\level{\entity}) \parallel \prod_{\alpha \in  \Reac} \TA(\alpha) \parallel \prod_{\beta \in \Syn} \TA(\beta) \parallel \TA_{\tick} \]  
 where $\TA(\entity, \level{\entity})$, $\TA(\alpha)$,$\TA(\beta)$  and $\TA_{\tick}$ are defined next. In the following we assume $ \Tag $ to be the set of identifiers of \obligatory activities in $\Syn$. 
 \paragraph{\bf Entities.}
 $\TA(\entity, \level{\entity}) = (L_{\entity},l^0_{\entity},X_{\entity},\Sigma_{\entity}, \arcs_{\entity} ,\inv_{\entity})$
  where:
  \begin{itemize}
   \item $L_{\entity}=\{l^{\entity}_i \mid i \in [0 \mydots \setlev_{\entity} ]\} \cup \{k_i^h,k_i^{d,h} \mid i \in [0 \mydots \setlev_{\entity} ], h\in \Tag^{\circledast} \}$ with  $l^0_{\entity} = l^{\entity}_{\level{\entity}}$
   \item $X_{\entity}=\{\birth^{\entity}_i, \refr^{\entity}_i \mid i \in [0 \mydots \setlev_{\entity} ]\} \cup \{x_{\entity}\}$
   \item $\Sigma^s_{\entity} =  \{  \alpha \mid \alpha \text{ identifier of an activity in }  \Reac  \}$, $  \Sigma_{\entity}^b =  \Tag^{\circledast}$, $\Sigma_{\entity}^u =  \{\tick h \mid h \in \Tag^{\circledast} \} $ 
   \item $\arcs_{\entity} = \arcs_{\Reac} \cup \arcs_{\Syn}$ where 
$$
\arcs_{\Reac}\! =\! \{ l_j \xrightarrow{g(A_{\alpha}) \wedge g(I_{\alpha}) \wedge x_{\entity} = 0, \alpha, r} l_e \mid \entity_{A_{\alpha}} \leq j < \entity_{I_{\alpha}}, \alpha \in \Reac, \entity \in A_{\alpha} \cup I_{\alpha} \cup R_{\alpha} \}  
$$
with  $j, e, \entity_{A_{\alpha}}$, and $\entity_{I_{\alpha}}$ are levels of $\entity$ defined as follows:
    
    $$\entity_{A_{\alpha}} = \begin{cases}
                \level{a} & \text{if } (\entity, \level{a}) \in {A_{\alpha}}     \\
                0 & \text{otherwise}
               \end{cases}
\qquad 
\entity_{I_{\alpha}} = \begin{cases}
               \level{i} & \text{if } (\entity, \level{i}) \in {I_{\alpha}}\\
                \setlev_{\entity} & \text{otherwise}
               \end{cases}
$$

$$ g(A_{\alpha}) = \begin{cases}
\birth^{\entity}_{\level{a}} \geq \dur{\alpha} & \text{if } (\entity, \level{a}) \in A_{\alpha}\\
           \true & \text{otherwise}
          \end{cases}
\ 
g(I_{\alpha}) = \begin{cases}
\birth^{\entity}_{\level{i}} \geq \dur{\alpha} & \text{if } (\entity, \level{i}) \in I_{\alpha}\\
           \true & \text{otherwise}
          \end{cases}
$$

$$e = \begin{cases}
               \max(0, \min(j+v, \setlev_{\entity}-1)) & \text{if } (\entity, v) \in R_{\alpha} \\
                j & \text{otherwise}
               \end{cases}
$$

$$r = \begin{cases}
        \emptyset & \text{if } (\entity, v) \not \in R_{\alpha}  \\
        \{u^\entity_e,\} \cup \{\birth_x^{\entity} \mid x \in [j+1,e]\} & \text{if } (\entity, v) \in R_{\alpha}  \wedge e-j>0\\
        \{u^\entity_e,\} & \text{if } (\entity, v) \in R_{\alpha}  \wedge e-j=0\\
        \{u^\entity_e,\} \cup \{\birth_x^{\entity} \mid x \in [e+1,j]\} & \text{if } (\entity, v) \in R_{\alpha}  \wedge e-j<0
      \end{cases}
$$
$$
\begin{array}{ll}
 \arcs_{\Syn} = & \{ l_j \xrightarrow{g(d)\wedge g , h?, \emptyset} k_j^{d,h},  \mid  j \in [0\mydots\setlev_{\entity}-1], h\in \Tag^{\circledast}\} \ \cup \\
               & \{ l_j \xrightarrow{\neg g(d)\wedge g , h?, \emptyset} k_j^h,  \mid  j \in [0\mydots\setlev_{\entity}-1], h\in \Tag^{\circledast}\} \ \cup \\
              & \{ k_j^{d,h} \xrightarrow{\true, h', r \cup \{x_{\entity}\} } l_e,  \mid  j \in [0\mydots\setlev_{\entity}-1], h,h' \in \Tag^{\circledast}, h<h' \}\ \cup \\ 
              & \{ k_j^h \xrightarrow{\true, \tick h', r'\cup \{x_{\entity}\} } l_e',  \mid  j \in [0\mydots\setlev_{\entity}-1], h,h' \in \Tag^{\circledast}, h<h' \}
\end{array}
$$
where
$$\begin{array}{lcl}
   g & = & \! \bigwedge_{k=1}^{n} g(\beta_k)  \wedge \bigwedge_{k=1}^{m} \neg g(\beta'_m)\text{ for } h=\beta_1 \cdots \beta_n \text{ and } h_1- h= \beta'_1 \cdots \beta'_m \\
   g(\beta) & = & g'(A_\beta) \wedge g'(I_\beta) \text{ and } \beta= \activ{A_\beta}{I_\beta}{\dur{\beta}}{R_\beta}\\
   g(d) & = & u_j > \life_{\entity}(j)
  \end{array}
$$    


$$ g'(A_\beta) = \begin{cases}
j \geq \level{a} \wedge \birth^{\entity}_{\level{a}} \geq \dur{\beta} & \text{if } (\entity, \level{a}) \in A_\beta\\
           \true & \text{otherwise}
          \end{cases}
$$
$$
g'(I_\beta) = \begin{cases}
j<\level{i} \wedge \birth^{\entity}_{\level{i}} \geq \dur{\beta} & \text{if } (\entity, \level{i}) \in I_\beta\\
           \true & \text{otherwise}
          \end{cases}
$$
$$
\begin{array}{lcl}
e & = & \max(0, \min(\sum_{i\in[1 \mydots n]} f(h[i]') +j -1, \setlev_{\entity}-1)) \\
e' & = & \max(0, \min(\sum_{i\in[1\mydots n]} f(h[i]')+j, \setlev_{\entity}-1)) \\
 & & \mbox{ where } f(h[i]) = \begin{cases}
        v & \text{if }  (\entity, v) \in R_{\beta_i} \\
        0 & \text{otherwise} 
       \end{cases}
\end{array}
$$
\[
\begin{array}{ll}
r = &\begin{cases}
        \{u^\entity_e\} \cup \{\birth_x^{\entity} \mid x \in [j+1,e]\} & \text{if }  e-j>0\\
        \{u^\entity_e\} & \text{if }   e-j=0 \\
        \{u^\entity_e\} \cup \{\birth_x^{\entity} \mid x \in [e+1,j]\} & \text{if }   e-j<0     
      \end{cases}
      \\
r' = &\begin{cases}
        \{u^\entity_{e'}\} \cup \{\birth_x^{\entity} \mid x \in [j+1,e']\} & \text{if }  e'-j>0\\
        \{u^\entity_{e'}\} & \text{if }  \entity \in h'  \wedge e'-j=0 \\
        \{u^\entity_{e'}\} \cup \{\birth_x^{\entity} \mid x \in [e'+1,j]\} & \text{if }   e'-j<0 \\
        \emptyset & \text{if }  \entity \notin h' 
      \end{cases}
\end{array}
     \]
where $\entity \in h$ denotes formula: $\exists \beta_k=\activ{A_{\beta_k}}{I_{\beta_k}}{\dur{\beta_k}}{R_{\beta_k}}$ s.t. $h=\beta_1\cdots \beta_n, 1\leq k \leq n \wedge (\entity, v) \in R_{\beta_k}$ 
    
   \item $Inv_{\entity}(l^{\entity}_i) = \refr^{\entity}_i \leq \life_{\entity}(i)$ for all $i \in [0 \mydots \setlev_{\entity}]$
   
  \end{itemize}

  \paragraph{\bf \Potential activity.}
$\TA(\alpha) = (L_{\alpha},l^0_{\alpha},X_{\alpha},\Sigma_{\alpha},\arcs_{\alpha},\inv_{\alpha})$  for $\alpha \in \Reac$ where
  \begin{itemize}
  \item $L_{\alpha}=\{l_\alpha\}$,  $l^0_{\alpha} = \alpha$, $X_{\alpha}= \{w_{\alpha}\}$,  $\Sigma^s_{\alpha} = \{ \alpha \} $
  \item $\arcs_{\alpha} = \{ l_\alpha \xrightarrow{w_{\alpha} \geq  \dur{\alpha}, \alpha, \{ w_{\alpha}\}} l_\alpha \}$
  \item $\inv_{\alpha}(l_{\alpha}) = \true$.
  \end{itemize}
  
  \paragraph{\bf \Obligatory activity.} $\TA(\beta) = (L_{\beta},l^0_{\beta},X_{\beta},\Sigma_{\beta},\arcs_{\beta},\inv_{\beta})$  for $\beta \in \Syn$ where
  \begin{itemize}
   \item $L_{\beta}=\{l_\beta, l'_\beta\}$,  $l^0_{\beta} = l_\beta$,  $X_{\beta}= \{w_{\beta}\}$,  $\Sigma_{\beta}^b =  \Tag^{\circledast}$,  $
\Sigma_{\beta}^u =  \{ \tick h \mid h\in \Tag^{\circledast}\} $
   \item $\arcs_{\beta} = \{ l_\beta \xrightarrow{w_{\beta} \geq  \dur{\beta}, h?, \emptyset} l'_\beta \mid h\in \Tag^{\circledast}, \beta\in h \} \cup \{ l'_\beta \xrightarrow{\true, \tick h, \{w_{\beta}\}} l'_\beta \mid h\in \Tag^{\circledast}, \beta\in h \}$
   \item $\inv_{\beta}(l_{\beta}) = \true$ and $\inv_{\beta}(l'_{\beta}) = \true$.
  
  \end{itemize}
  
  \paragraph{\bf Time.}  $\TA_{\tick} = (L_{\tick},l^0_{\tick},X_{\tick},\Sigma_{\tick},\arcs_{\tick},\inv_{\tick})$ where
  \begin{itemize}
   \item $L_{\tick}=\{l_h \mid h \in \Tag^{\circledast}\} \cup \{l_{\bot}\}$,  $l^0_{\tick} = l_{h_1}$,  $X_{\tick}= \{x\}$, $\Sigma_{\tick}^b =  \Tag^{\circledast}$, $ 
\Sigma_{\tick}^u =  \{ \tick h \mid h\in \Tag^{\circledast}\} $
   \item $\arcs_{\tick} =\begin{array}{l}
 \{l_{h_i} \xrightarrow{x=1, h_i!, \emptyset } l_{h_i+1}, l_{h_i+1} \xrightarrow{\true, \tick h_i, \{x\} } l_{h_1} \mid h,  i \in [1\mydots n-1]   \}  \\
\cup \ \{ l_{h_n} \xrightarrow{x=1, h_n!, \emptyset } l_{\bot}, l_{\bot} \xrightarrow{\true, \tick\varepsilon, \{x\} } l_{h_1}   \}
                  \end{array}
$
   \item $\inv_{\tick}(l) = \true$ for all $l \in L_{\tick}$.
  
  \end{itemize}
  
  
  
 \end{definition}

 We now comment on the definition of the encoding.
 For each entity $\entity$, the corresponding marking of place $p_{\entity}$, $M(p_{\entity})=\tuple{\lev_{\entity}, \refr_{\entity}, \birth_{\entity}}$, in the Petri net representation is encoded by    
 the state (location $l^{\entity}_{\lev_{\entity}}$ and valuations of clocks variables $\refr^{\entity}_{\lev_{\entity}}, \birth^{\entity}_i$ for $i \in [0\mydots\setlev_{\entity} -1]$) of each timed automaton $\TA(\entity, \level{\entity})$. Marking of places $p_{\rho}$ (for $\rho \in \Syn \cup \Reac$) is given by the valuation of clock $w_{\rho}$ in the corresponding timed automaton $\TA(\rho)$.
 
 Each transition of the Petri net is encoded by (a series of) timed automata arcs.
 For each transition $t_{\alpha}$ (corresponding to  \potential activity  $\alpha$) involving $\entity$ there is a (synchronous) arcs in the timed automaton $\TA(\entity, \level{\entity})$ whose guard describes its role in the activity (activator, inhibitor or result). Clock $w_{\alpha}$ in   $\TA(\alpha)$ implements the constraint that the activity $\alpha$ is performed at most once in the interval $\dur{\alpha} $:  $w_{\alpha} \geq \dur{\alpha}$. 
 This way, the synchronous product of all automata reconstructs the full guard of the activity $\alpha$ and  exactly one  transition in the synchronized product of automata corresponds to the firing of transition $t_{\alpha}$. The state reached after this transition coincides with the corresponding marking in the Petri net.
 
 Transition $t_c$ is trickier as time progression causes  decay but more importantly the simultaneous action of \obligatory activities.
 Notice that \obligatory activities concern the global state of an \andy network (the maximal set of enabled \obligatory activities has to be performed each time $t_c$ fires) but each sub-automaton of the synchronized automaton as only a partial/local information.  
 That is why, we need to introduce the auxiliary automaton $\TA_{\tick}$ that coordinates and gathers partial information from all  other automata.
 Thus, the implementation of $t_c$ has two phases. The first one gathers partial information, performs the selection of the largest set of enabled \obligatory activities and forces the time to progress in a discrete fashion;  the second phase completes the time progression and synchronizes all timed automata communicating the chosen maximal set of \obligatory activities.
 Both phases are initiated by   automaton $\TA_{\tick}$ which has two types of arcs: broadcast ones for the first phase and urgent synchronous ones for the second (see Figure \ref{fig:tick}).
\begin{figure}[t]
\centering
\begin{tikzpicture}[>=latex',xscale=1, yscale=.6,every node/.style={scale=0.7}]
\node[location,double] at (0,0) (l1) {$l_{\beta_1\beta_2}$}; 
\node[location]  at (2,0) (l2) {$l_{\beta_1}$};
\node[location]  at (4,0) (l3) {$l_{\beta_2}$};
\node[location]  at (6,0) (l4) {$l_{\epsilon}$};
\node[location]  at (8,0) (l5) {$l_{\bot}$};
\draw[->] (l1) -- node[midway,above] {$\beta_1\beta_2!$} (l2) ;
\draw[->] (l2) -- node[midway,above] {$\beta_1!$} (l3) ;
\draw[->] (l3) -- node[midway,above] {$\beta_2!$} (l4) ;
\draw[->] (l4) -- node[midway,above] {$\epsilon!$} (l5) ;
\draw[->, rounded corners] (l2) -- node[midway,right] {$\tick\beta_1\beta_2$}(2,1.5) -- (1,1.5) --  (l1) ;
\draw[->, rounded corners] (l3) -- node[midway,right] {$\tick\beta_1$}(4,2) -- (1,2) --  (l1) ;
\draw[->, rounded corners] (l4) -- node[midway,right] {$\tick\beta_2$}(6,2.5) -- (1,2.5) --  (l1) ;
\draw[->, rounded corners] (l5) -- node[midway,right] {$\tick\epsilon$}(8,3) -- (1,3) --  (l1) ;

\end{tikzpicture}
\caption{The shape of timed automaton $\TA_\tick$ for $\Tag^\circledast=\{\beta_1\beta_2,\beta_1,\beta_2,\epsilon\}$, where $\tick\beta_1\beta_2$, $\tick\beta_1$, $\tick\beta_2$, $\tick\epsilon$ are all synchronous urgent communication labels.}
\label{fig:tick}
\end{figure}
More precisely, $\TA_{\tick}$ progressively interrogates the entities timed automata $\TA(\entity, \level{\entity})$ and the \obligatory activities automata $\TA(\beta_i)$ to ``compute'' for each automaton the maximal set of enabled \obligatory activities. This is obtained through broadcast arcs labeled with sequences of \obligatory activities identifiers $h\in\Tag^\circledast$, from the longest ($h=seq(\Tag)=\beta_1\cdots\beta_n$) to the shortest ($h=\epsilon$, \ie no \obligatory activity is enabled).
 As broadcast is a non blocking transition and because of the ordering on sequences in $\Tag^\circledast$, each entity automaton chooses its maximal set of \obligatory activities it is involved in. If it is necessary, it also performs decay. When all automata $\TA(\entity, \level{\entity})$ and $\TA(\beta_{i})$ have agreed on some sequence $h=\beta_{i_1} \mydots \beta_{i_m}$ (in the worst case $h$ is empty) the first phase is completed and $\{ \beta_{i_1},  \mydots,  \beta_{i_m}\}$ is the largest set of enabled \obligatory activities. The second phase is then implemented with an urgent synchronous arc synchronizing all automata: $\TA_{\tick}$, $\TA(\entity, \level{\entity})$, for each $\entity \in \entities$, and $\TA(\beta_i)$, for $i\in [i_1 \mydots i_m]$.
 Notice that guards on broadcast transitions constraint the clocks to progress by one time unit at once.   
 As a consequence, at the end of the two phase algorithm, timed automata of entities and of places $p_{\rho}$ together with the  corresponding clocks valuations exactly encode the marking reached after firing $t_c$.
Thus we can get the following correctness theorem:
 
  \begin{theorem}
The encoding of  \andy network $(\entities, \Syn, \Reac)$
%its encoding $\enc{(\entities, \Syn, \Reac)}$, 
is correct and complete.\looseness=-1
\end{theorem}
\begin{proof}[sketch]
 Follows by induction on the length of the run and from a case analysis on the transition performed. \qed
\end{proof}
 


\section{Conclusion, Related and Future Work}\label{sec:concl}


We have introduced \andy, a high-level Petri net framework to model
time-dependent activity-driven systems. In \andy, systems consist of a set of entities
present in the environment at a given level. Entities can age as time
passes by and their level is governed by a set of \obligatory and \potential activities with duration. 
%In an activity, entities can have the role of activators, inhibitors and
%results. 
%An activity has a given duration. 
 %and it can take place only if
%all activators are available and all inhibitors are not for the whole
%duration of the activity. Depending on the type of activity, results
%levels are either increased, maintained or decreased. 
In order to asses the handling of time, we have presented an alternative formulation, with  equivalent semantics, of \andy networks into a suitable class of timed automata. 

From a technical point of view, the closest related work is on reaction
systems \cite{DBLP:journals/ijfcs/BrijderEMR11} or their Petri net
representation \cite{koutnyreaction}. Although we use a similar
definition for activity, the semantics we have proposed is inherently
different: in \cite{DBLP:journals/ijfcs/BrijderEMR11} all enabled
reactions occur in one step while we consider two forms of activity evolution: simultaneous  for \obligatory activities and
interleaved for \potential ones.
%%
Furthermore, we have introduced discrete abstract  levels that, to the
best of our knowledge, are not taken into account in reaction systems. 
Also, we have presented a more elaborated notion of time that governs
both entities and activity. 
%%
In  \cite{DBLP:conf/birthday/BrijderER11}, the authors consider an
extension of reaction systems with duration but it concerns only decay
and not  duration of activities. Furthermore the decay is  referred to
the number of steps and not to the discrete time progression as in our case.\looseness=-1  

From the Petri net modeling point of view, our representation of time is considerably different from the approaches traditionally used in time and timed Petri nets 
(\cite{DBLP:journals/tcs/CeroneM99} presents a survey with insightful
comparison of the different approaches).
%%
The main difference lies on the fact that the  progression of time is implicit and  external to the system. By contrast, in our proposal we have assumed the presence of  an explicit way of incrementing durations (modeled by synchronized counters). 
This is also  different from the notion of timestamps introduced in  \cite{timestamp} that again refers to an implicit notion of time.
Indeed,  our approach is conceptually closer to Petri nets with causal time  \cite{DBLP:journals/entcs/ThanhKP02} for the presence of an explicit transition for time progression. Nevertheless, in our approach time cannot be suspended under the influence of the environment (as is the case in \cite{DBLP:journals/entcs/ThanhKP02}).\looseness=-1
%%
 
In a broader sense, our work could also be related to P-systems
\cite{DBLP:journals/ijfcs/PaunPRS11,DBLP:journals/fuin/KleijnK11} or the
$\kappa$-calculus \cite{DBLP:journals/tcs/DanosL04} that  describe the
evolution of cells through rules. 
%%
Both these approaches are mainly oriented to simulation while we are
interested in  verification aspects. Finally, always related to the
modeling in Petri nets but with a different aim, levels have been used
in qualitative approaches to address problems related to the
identification of steady states in genetic networks such as in
\cite{DBLP:journals/nc/ChaouiyaNRT11}. 
Similarly in workflow modeling, several models have been proposed \cite{DBLP:conf/dfg/EshuisW03}.
Nevertheless these contributions
abstract away from time related aspects that are instead central in our
proposal.  


The main application of our work concerns the verification of properties
of systems defined in terms of  activities. We have prototyped a
tool to simulate and build the state space of an \andy network relying on the 
high-level Petri net semantics and using the SNAKES
toolkit~\cite{Pom-PNN-2008}, see for example Appendix~\ref{app:mobile}. We
have also developed an alternative implementation using the MGS
framework~\cite{giavitto2008} to test several strategies that can be
used to avoid the combinatorial explosion and to build lazily the state
space. These tools have been effectively used in the analysis of several
applications: in physiology (modeling the metabolism of glucose), in the
modeling of regulatory network (\eg the repressilator),
etc. (see Appendix \ref{app:repr}). %The results will be reported elsewhere.
%
The first results are very positive and we plan to develop the \andy
approach along several directions. We want to extend decay function to arbitrary maps in $\setlev$. The
problem is to generalize the notion of increase and decrease in a
relevant way for the application. More structure can also be given to
the notion of entity. Characterizing an entity by several attributes
(instead of only one level), raises the question of the causal
relationships between these attributes and their update
strategy. Another aspect will be addressed in the future: we shall
consider dynamic models where entities are created and deleted, as
in~\cite{Giavitto2012}. Finally, we are also working on more efficient
translation towards timed automata to make possible the use of
model-checking tools like UPPAAL \cite{uppaal} on more significant examples.




%% 
%Related: reaction systems, petri nets with causal time and petri nets with timestamps
%

% \vspace{-0.2cm}
% \paragraph{\bf Acknowledgments.}
% This work was supported by the French project ANR BLANC 0307 01 -
% SYNBIOTIC. We thanks F. Pommereau for useful discussions and his help in
% the use of the SNAKES toolkit. 
%  
% \vspace{-0.4cm}
{\small
\bibliographystyle{abbrv}
\bibliography{biblio}
}
\appendix





\section{Example of a High-level Petri Net}\label{app:exfiring}

Here we detail a simple example of firing. Let this be the state of the Petri net before the transition:
\begin{center}
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=45,auto]

  \node [place, label = left: $p_1$] at (-1.5,0) (Q1){$7$};
  \node [place, label=left:$p_2$]at (0,-1.5)  (Q2){$5$};
  \node [place, label = right: $p_3$] at (1.5,0) (Q3){};
  
  \node [transition] (t) [  label={[red] above:$\begin{array}{c}
                                                x>y ~\wedge \\ x'=x+y
                                               \end{array}$}] at (0,0) {$t$}
   edge [pre]    node[below] {$x$}    (Q1)
   edge [pre]    node[right] {$y$}    (Q2)
   edge [post]   node[below]{$x'$}    (Q3);
\end{tikzpicture}
\end{center}
then by letting $\sigma = \{ x= 7, y=5, x'=12\}$,  after the firing we obtain 
\begin{center}
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=45,auto]

  \node [place, label = left: $p_1$] at (-1.5,0) (Q1){};
  \node [place, label=left:$p_2$]at (0,-1.5)  (Q2){};
  \node [place, label = right: $p_3$] at (1.5,0) (Q3){12};
  
  \node [transition] (t) [  label={[red] above:$\begin{array}{c}
                                                x>y~\wedge \\ x'=x+y
                                               \end{array}$}] at (0,0) {$t$}
   edge [pre]    node[below] {$x$}    (Q1)
   edge [pre]    node[right] {$y$}    (Q2)
   edge [post]   node[below]{$x'$}    (Q3);
\end{tikzpicture}
\end{center}



\section{Example of a Timed Automaton}\label{app:ta}
%\begin{figure}[htbp]
%\centering
%\subfigure[$\TA_1\parallel \TA_2$]{
Here we exemplify timed automata usage: 
consider for instance the network of timed automata $\TA_1$ and $\TA_2$ with synchronous (non urgent) communications only:
\begin{center}
\begin{tikzpicture}[>=latex',xscale=.8, yscale=.6,every node/.style={scale=0.7}]
\node[location,double] at (0,0) (l1) {$\stackrel{l_1}{x < 2}$}; 
\node[location]  at (4,0) (l2) {$\stackrel{l_2}{x < 2}$};
\node[left] at (-4,0) {$\TA_1$};
\node[location,double] at (0,-2) (l3) {$\stackrel{l_3}{\emptyset}$};
\node[location] at (4,-2) (l4) {$\stackrel{l_4}{\emptyset}$};
\draw[->, rounded corners] (l2) -- (5,-.5) -- (5.5,-.5) -- node[midway,right] 
				{$x>0;b;\emptyset$}  (5.5,.5) -- (5,.5)-- (l2) ;

\node[left] at (-4,-2) {$\TA_2$};
\draw[->] (l1) -- (l2) node[midway,above] {$x=1;a;\{x\}$};
\draw[->] (l3) -- (l4) node[midway,above] {$x=1;c;\emptyset$};
\draw[->, rounded corners] (l3) -- (-1,-2.5) -- (-1.5,-2.5) -- node[midway,left] 
				{$\true;a;\{x\}$}  (-1.5,-1.5) -- (-1,-1.5)-- (l3) ;
\end{tikzpicture}
\end{center}
%}
%%%
%\subfigure[$sync(\TA_1\parallel \TA_2)$]{
whose behavior is given by their synchronized product $\TA_1\parallel \TA_2$:
\begin{center}
\begin{tikzpicture}[>=latex',xscale=.9, yscale=.6,every node/.style={scale=0.7}]
\node[location]  at (0,0) (l14) {$\stackrel{(l_1,l_4)}{x < 2}$};
\node[location,double] at (3,0) (l13) {$\stackrel{(l_1,l_3)}{x < 2}$}; 
\node[location] at (6,0) (l23) {$\stackrel{(l_2,l_3)}{x < 2}$};
\node[location] at (9,0) (l24) {$\stackrel{(l_2,l_4)}{x < 2}$};
\draw[->, rounded corners] (l23) -- (5.5,1) -- (5.5,1.5) -- node[midway,above] 
				{$x>0;b;\emptyset$}  (6.5,1.5) -- (6.5,1)-- (l23) ;
\draw[->] (l13) -- (l14) node[midway,above] {$x=1;c;\emptyset$};
\draw[->] (l13) -- (l23) node[midway,above] {$x=1;a;\{x\}$};
\draw[->] (l23) -- (l24) node[midway,above] {$x=1;c;\emptyset$};
\draw[->, rounded corners] (l24) -- (8.5,1) -- (8.5,1.5) -- node[midway,above] 
				{$x>0;b;\emptyset$}  (9.5,1.5) -- (9.5,1)-- (l24) ;
\end{tikzpicture}
\end{center}
%}
%%%
%HK doit être modifié pour inclure des canaux broadcast
%\subfigure[A possible run]{
and where a possible run is:
\begin{center}
\begin{tikzpicture}[>=latex',xscale=1, yscale=.6,every node/.style={scale=0.7}]
\node at (0,0) (e1) {$[(l_1,l_3);x=0]$}; // t+1
\node at (2,0) (e2) {$[(l_1,l_3);x=1]$}; // a
\node at (4,0) (e3) {$[(l_2,l_3);x=0]$}; // t+.5
\node at (6,0) (e4) {$[(l_2,l_3);x=.5]$}; // b
\node at (8,0) (e5) {$[(l_2,l_3);x=.5]$}; // t+.5
\node at (10,0) (e6) {$[(l_2,l_4);x=1]$}; 
\draw[->] (e1) -- (e2) ;
\draw[->] (e2) -- (e3) ;
\draw[->] (e3) -- (e4) ;
\draw[->] (e4) -- (e5) ;
\draw[->] (e5) -- (e6) ;
\end{tikzpicture}
\end{center}
%}
%\caption{A network of timed automata with a possible run.}
%\label{fig:ta}
%\end{figure}




\section{Mobile Phone Battery}\label{app:mobile}
Here we show the SNAKES rendering of the mobile phone example:

{\centering
\scalebox{0.33}{
\begin{tikzpicture}[>=latex',line join=bevel,scale=0.7]
%%
\definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_13) at (1218.6bp,361bp) [draw,fill=fillcolor,rectangle] {tr1};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_14) at (1206.6bp,151bp) [draw,fill=fillcolor,rectangle] {tr0};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_18) at (943.65bp,571bp) [draw,fill=fillcolor,rectangle] {tc: True};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_19) at (714.65bp,361bp) [draw,fill=fillcolor,rectangle] {tr4};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_9) at (1393.6bp,676bp) [draw,fill=fillcolor,ellipse] {ptr0: \{0\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_8) at (331.65bp,466bp) [draw,fill=fillcolor,ellipse] {ptr3: \{0\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_7) at (520.65bp,46bp) [draw,fill=fillcolor,ellipse] {ptr2: \{0\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_6) at (851.65bp,466bp) [draw,fill=fillcolor,ellipse] {pob2: \{0\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_5) at (1006.6bp,466bp) [draw,fill=fillcolor,ellipse] {ptr4: \{0\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_4) at (103.65bp,466bp) [draw,fill=fillcolor,ellipse] {pob0: \{0\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_3) at (219.65bp,466bp) [draw,fill=fillcolor,ellipse] {pob1: \{0\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_2) at (699.65bp,256bp) [draw,fill=fillcolor,ellipse] {G: \{(0, 0, (0, 0))\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_1) at (663.65bp,466bp) [draw,fill=fillcolor,ellipse] {B: \{(4, 0, (0, 0, 0, 0, 0))\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_0) at (183.65bp,256bp) [draw,fill=fillcolor,ellipse] {C: \{(0, 0, (0, 0))\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_17) at (745.65bp,151bp) [draw,fill=fillcolor,rectangle] {tr5};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_11) at (887.65bp,46bp) [draw,fill=fillcolor,ellipse] {ptr5: \{0\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_16) at (282.65bp,151bp) [draw,fill=fillcolor,rectangle] {tr2};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_10) at (1226.6bp,466bp) [draw,fill=fillcolor,ellipse] {ptr1: \{0\}};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_15) at (209.65bp,361bp) [draw,fill=fillcolor,rectangle] {tr3};
  \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
  \node (node_12) at (1158.6bp,256bp) [draw,fill=fillcolor,ellipse] {P: \{(0, 0, (0, 0))\}};
  \draw [->,solid] (node_4) ..controls (53.011bp,500.46bp) and (38.13bp,517.88bp)  .. (51.647bp,532bp) .. controls (81.223bp,562.9bp) and (723bp,569.51bp)  .. (node_18);
  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
  \pgfsetstrokecolor{strokecol}
  \draw (75.647bp,523bp) node { $wob_0$};
  \draw [->,solid] (node_18) ..controls (1038.5bp,561.15bp) and (1159.3bp,546.66bp)  .. (1171.6bp,532bp) .. controls (1176.8bp,525.88bp) and (1175.9bp,520.78bp)  .. (1171.6bp,514bp) .. controls (1161.9bp,498.5bp) and (1148.7bp,507.72bp)  .. (1134.6bp,496bp) .. controls (1109.3bp,474.81bp) and (1118.7bp,453.59bp)  .. (1090.6bp,436bp) .. controls (1053.5bp,412.68bp) and (1021.7bp,451.71bp)  .. (993.65bp,418bp) .. controls (993.65bp,418bp) and (993.65bp,340bp)  .. (993.65bp,340bp) .. controls (970.26bp,310.93bp) and (935.71bp,350.52bp)  .. (911.65bp,322bp) .. controls (897.88bp,305.68bp) and (905.03bp,151.22bp)  .. (902.65bp,130bp) .. controls (901bp,115.31bp) and (898.36bp,99.311bp)  .. (node_11);
  \draw (969.65bp,313bp) node { min(D,wtr5+1)};
  \draw [->,solid] (node_5) ..controls (964.3bp,442.46bp) and (955.34bp,438.64bp)  .. (946.65bp,436bp) .. controls (885.78bp,417.51bp) and (864.51bp,439.53bp)  .. (804.65bp,418bp) .. controls (785.12bp,410.97bp) and (765.42bp,399.16bp)  .. (node_19);
  \draw (815.65bp,409bp) node { w};
  \draw [->,solid] (node_9) ..controls (1265.4bp,646.08bp) and (1074.2bp,601.47bp)  .. (node_18);
  \draw (1204.1bp,619bp) node { wtr0};
  \draw [->,solid] (node_19) ..controls (733.51bp,329.2bp) and (737.44bp,315.93bp)  .. (733.65bp,304bp) .. controls (732.5bp,300.38bp) and (730.96bp,296.8bp)  .. (node_2);
  \draw (798.15bp,313bp) node { ($l_G$,$u_G$,$\lambda_G$)};
  \draw [->,solid] (node_18) ..controls (976.99bp,539.38bp) and (983.9bp,526.2bp)  .. (977.65bp,514bp) .. controls (971.41bp,501.81bp) and (961.45bp,506.49bp)  .. (952.65bp,496bp) .. controls (933.6bp,473.32bp) and (948.29bp,452.43bp)  .. (923.65bp,436bp) .. controls (893.74bp,416.06bp) and (636.01bp,424.46bp)  .. (600.65bp,418bp) .. controls (574.51bp,413.22bp) and (569.43bp,406.41bp)  .. (543.65bp,400bp) .. controls (522.16bp,394.66bp) and (459.82bp,399.01bp)  .. (445.65bp,382bp) .. controls (433.7bp,367.66bp) and (433.43bp,354.12bp)  .. (445.65bp,340bp) .. controls (482.09bp,297.89bp) and (519.87bp,346.96bp)  .. (569.65bp,322bp) .. controls (579.76bp,316.93bp) and (578.28bp,310.34bp)  .. (587.65bp,304bp) .. controls (600.65bp,295.2bp) and (615.53bp,287.46bp)  .. (node_2);
  \draw (663.15bp,409bp) node { ($l_G$,$u_G$,$\lambda_G$)};
  \draw [->,solid] (node_10) ..controls (1302.9bp,485.07bp) and (1346.3bp,499.1bp)  .. (1356.6bp,514bp) .. controls (1361.2bp,520.56bp) and (1362bp,526.08bp)  .. (1356.6bp,532bp) .. controls (1332.2bp,558.88bp) and (1089.5bp,567.62bp)  .. (node_18);
  \draw (1382.1bp,523bp) node { wtr1};
  \draw [->,solid] (node_8) ..controls (299.73bp,426.93bp) and (285.77bp,411.83bp)  .. (271.65bp,400bp) .. controls (266.54bp,395.72bp) and (260.92bp,391.56bp)  .. (node_15);
  \draw (300.65bp,409bp) node { w};
  \draw [->,solid] (node_18) ..controls (820.19bp,564.49bp) and (585.46bp,550.33bp)  .. (555.65bp,532bp) .. controls (502.72bp,499.46bp) and (554.78bp,442.7bp)  .. (509.65bp,400bp) .. controls (477.16bp,369.26bp) and (445.07bp,410.55bp)  .. (410.65bp,382bp) .. controls (382.83bp,358.93bp) and (372.19bp,336.67bp)  .. (387.65bp,304bp) .. controls (427.23bp,220.36bp) and (509.06bp,255.64bp)  .. (548.65bp,172bp) .. controls (562.05bp,143.68bp) and (552.46bp,108.7bp)  .. (node_7);
  \draw (445.65bp,313bp) node { min(D,wtr2+1)};
  \draw [->,solid] (node_14) ..controls (1381.8bp,177.1bp) and (1399.4bp,183.04bp)  .. (1408.6bp,190bp) .. controls (1435.1bp,209.78bp) and (1442.6bp,223bp)  .. (1442.6bp,256bp) .. controls (1442.6bp,571bp) and (1442.6bp,571bp)  .. (1442.6bp,571bp) .. controls (1442.6bp,597.2bp) and (1438.7bp,604.26bp)  .. (1427.6bp,628bp) .. controls (1425.6bp,632.45bp) and (1423.1bp,636.92bp)  .. (node_9);
  \draw (1452.1bp,409bp) node { 0};
  \draw [->,solid] (node_17) ..controls (795.99bp,113.78bp) and (825.8bp,91.734bp)  .. (node_11);
  \draw (831.15bp,103bp) node { 0};
  \draw [->,solid] (node_12) ..controls (1226bp,284.82bp) and (1235.5bp,293.33bp)  .. (1241.6bp,304bp) .. controls (1246.5bp,312.37bp) and (1245bp,321.95bp)  .. (node_13);
  \draw (1309.1bp,313bp) node { ($l_P$, $u_P$, $\lambda_P$)};
  \draw [->,solid] (node_17) ..controls (743.02bp,183.28bp) and (740.52bp,196.75bp)  .. (735.65bp,208bp) .. controls (733.99bp,211.82bp) and (731.98bp,215.61bp)  .. (node_2);
  \draw (804.15bp,199bp) node { ($l_G$,$u_G$,$\lambda_G$)};
  \draw [->,solid] (node_13) ..controls (1135.3bp,334.36bp) and (1123.9bp,328.18bp)  .. (1119.6bp,322bp) .. controls (1113.1bp,312.37bp) and (1115.6bp,301.62bp)  .. (node_12);
  \draw (1178.6bp,313bp) node { ($l_P$,$u_P$,$\lambda_P$)};
  \draw [->,solid] (node_16) ..controls (405.16bp,125.01bp) and (421.12bp,119.11bp)  .. (435.65bp,112bp) .. controls (454.06bp,103bp) and (472.29bp,89.591bp)  .. (node_7);
  \draw (473.15bp,103bp) node { 0};
  \draw [->,solid] (node_18) ..controls (1080.2bp,569.57bp) and (1378.7bp,563.5bp)  .. (1407.6bp,532bp) .. controls (1413.1bp,526.11bp) and (1411.5bp,521.02bp)  .. (1407.6bp,514bp) .. controls (1398.1bp,496.64bp) and (1267.1bp,435.36bp)  .. (1257.6bp,418bp) .. controls (1253.8bp,410.98bp) and (1252.4bp,406.08bp)  .. (1257.6bp,400bp) .. controls (1291.6bp,360.38bp) and (1338.7bp,420.76bp)  .. (1373.6bp,382bp) .. controls (1396.9bp,356.23bp) and (1398.4bp,331.04bp)  .. (1376.6bp,304bp) .. controls (1360.5bp,283.92bp) and (1302.4bp,271.75bp)  .. (node_12);
  \draw (1316.6bp,409bp) node { ($l_P$,$u_P$,$\lambda_P$)};
  \draw [->,solid] (node_11) ..controls (908.91bp,100.58bp) and (925.29bp,139.6bp)  .. (942.65bp,172bp) .. controls (975.6bp,233.51bp) and (1006.8bp,237.41bp)  .. (1027.6bp,304bp) .. controls (1042.8bp,352.38bp) and (999bp,379.22bp)  .. (1031.6bp,418bp) .. controls (1056.8bp,447.87bp) and (1087.2bp,411.53bp)  .. (1117.6bp,436bp) .. controls (1140.4bp,454.32bp) and (1124.6bp,474.67bp)  .. (1144.6bp,496bp) .. controls (1156.3bp,508.47bp) and (1169.8bp,499.35bp)  .. (1178.6bp,514bp) .. controls (1182.8bp,520.85bp) and (1183.8bp,525.9bp)  .. (1178.6bp,532bp) .. controls (1166.5bp,546.34bp) and (1053bp,559.99bp)  .. (node_18);
  \draw (1053.1bp,313bp) node { wtr5};
  \draw [->,solid] (node_18) ..controls (784.54bp,566.41bp) and (356.04bp,552.46bp)  .. (335.65bp,532bp) .. controls (328.73bp,525.06bp) and (325.98bp,515.41bp)  .. (node_8);
  \draw (393.65bp,523bp) node { min(D,wtr3+1)};
  \draw [->,solid] (node_0) ..controls (85.22bp,284.04bp) and (60.359bp,300.25bp)  .. (76.647bp,322bp) .. controls (80.619bp,327.3bp) and (89.039bp,332.13bp)  .. (node_15);
  \draw (141.65bp,313bp) node { ($l_C$, $u_C$, $\lambda_C$)};
  \draw [->,solid] (node_15) ..controls (210.44bp,328.99bp) and (209.61bp,315.62bp)  .. (206.65bp,304bp) .. controls (205.84bp,300.82bp) and (204.81bp,297.6bp)  .. (node_0);
  \draw (270.15bp,313bp) node { ($l_C$,$u_C$,$\lambda_C$)};
  \draw [->,solid] (node_7) ..controls (444.49bp,79.598bp) and (384.15bp,106.22bp)  .. (node_16);
  \draw (420.65bp,103bp) node { w};
  \draw [->,solid] (node_15) ..controls (227.95bp,393.76bp) and (237.57bp,407.73bp)  .. (248.65bp,418bp) .. controls (252.21bp,421.31bp) and (269.82bp,431.6bp)  .. (node_8);
  \draw (258.15bp,409bp) node { 0};
  \draw [->,solid] (node_12) ..controls (1115.8bp,300.47bp) and (1097.9bp,318.64bp)  .. (1093.6bp,322bp) .. controls (1081.4bp,331.62bp) and (1073.9bp,328.31bp)  .. (1063.6bp,340bp) .. controls (1050.6bp,354.9bp) and (1028.8bp,407.59bp)  .. (1037.6bp,418bp) .. controls (1068.8bp,454.82bp) and (1106.3bp,406.8bp)  .. (1144.6bp,436bp) .. controls (1168.1bp,453.82bp) and (1151.9bp,475.13bp)  .. (1172.6bp,496bp) .. controls (1175.1bp,498.48bp) and (1236.5bp,502.11bp)  .. (1210.6bp,532bp) .. controls (1196.3bp,548.59bp) and (1060bp,561.78bp)  .. (node_18);
  \draw (1101.1bp,409bp) node { ($l_P$, $u_P$, $\lambda_P$)};
  \draw [->,solid] (node_0) ..controls (282.79bp,277.88bp) and (311.35bp,288.61bp)  .. (334.65bp,304bp) .. controls (352.26bp,315.64bp) and (356.57bp,320.93bp)  .. (365.65bp,340bp) .. controls (380.78bp,371.8bp) and (360.63bp,388.35bp)  .. (379.65bp,418bp) .. controls (419.98bp,480.89bp) and (467.54bp,458.58bp)  .. (517.65bp,514bp) .. controls (523.78bp,520.79bp) and (519.98bp,527bp)  .. (527.65bp,532bp) .. controls (558.26bp,551.99bp) and (798.68bp,564.68bp)  .. (node_18);
  \draw (444.65bp,409bp) node { ($l_C$, $u_C$, $\lambda_C$)};
  \draw [->,solid] (node_2) ..controls (604.93bp,226.72bp) and (581.75bp,210.63bp)  .. (597.65bp,190bp) .. controls (601.83bp,184.57bp) and (610.33bp,179.75bp)  .. (node_17);
  \draw (664.65bp,199bp) node { ($l_G$, $u_G$, $\lambda_G$)};
  \draw [->,solid] (node_18) ..controls (760.09bp,567.16bp) and (169.47bp,553.4bp)  .. (136.65bp,532bp) .. controls (126.77bp,525.56bp) and (119.73bp,515.22bp)  .. (node_4);
  \draw (160.65bp,523bp) node { $wob_0$};
  \draw [->,solid] (node_11) ..controls (822.18bp,63.667bp) and (794.36bp,75.603bp)  .. (774.65bp,94bp) .. controls (766.85bp,101.27bp) and (760.83bp,111.11bp)  .. (node_17);
  \draw (785.65bp,103bp) node { w};
  \draw [->,solid] (node_14) ..controls (1223.1bp,183.15bp) and (1226.2bp,196.75bp)  .. (1220.6bp,208bp) .. controls (1217.9bp,213.69bp) and (1214bp,218.91bp)  .. (node_12);
  \draw (1282.6bp,199bp) node { ($l_P$,$u_P$,$\lambda_P$)};
  \draw [->,solid] (node_18) ..controls (749.02bp,569.86bp) and (73.172bp,563.87bp)  .. (42.647bp,532bp) .. controls (-27.86bp,458.37bp) and (-3.6588bp,376.85bp)  .. (67.647bp,304bp) .. controls (78.465bp,292.95bp) and (92.197bp,284.33bp)  .. (node_0);
  \draw (66.147bp,409bp) node { ($l_C$,$u_C$,$\lambda_C$)};
  \draw [->,solid] (node_16) ..controls (178.59bp,177.36bp) and (166.45bp,183.4bp)  .. (161.65bp,190bp) .. controls (155.67bp,198.2bp) and (155.99bp,208.13bp)  .. (node_0);
  \draw (222.15bp,199bp) node { ($l_C$,$u_C$,$\lambda_C$)};
  \draw [->,solid] (node_5) ..controls (996.74bp,507.27bp) and (991.71bp,520.89bp)  .. (984.65bp,532bp) .. controls (982.39bp,535.54bp) and (979.75bp,538.99bp)  .. (node_18);
  \draw (1015.1bp,523bp) node { wtr4};
  \draw [->,solid] (node_18) ..controls (966.39bp,604.78bp) and (979.81bp,619.84bp)  .. (995.65bp,628bp) .. controls (1054.2bp,658.14bp) and (1243.5bp,669.95bp)  .. (node_9);
  \draw (1053.6bp,619bp) node { min(D,wtr0+1)};
  \draw [->,solid] (node_19) ..controls (725.25bp,394.71bp) and (733.12bp,409.78bp)  .. (745.65bp,418bp) .. controls (783.13bp,442.61bp) and (903.5bp,423.76bp)  .. (946.65bp,436bp) .. controls (952.32bp,437.61bp) and (958.09bp,439.75bp)  .. (node_5);
  \draw (755.15bp,409bp) node { 0};
  \draw [->,solid] (node_1) ..controls (683.76bp,508.72bp) and (694.11bp,523.26bp)  .. (707.65bp,532bp) .. controls (738.58bp,551.97bp) and (839.92bp,562.99bp)  .. (node_18);
  \draw (772.65bp,523bp) node { ($l_B$, $u_B$, $\lambda_B$)};
  \draw [->,solid] (node_13) ..controls (1216.3bp,387.85bp) and (1215.9bp,394.16bp)  .. (1215.6bp,400bp) .. controls (1215.3bp,407.99bp) and (1214.7bp,410.05bp)  .. (1215.6bp,418bp) .. controls (1216bp,420.87bp) and (1216.4bp,423.81bp)  .. (node_10);
  \draw (1225.1bp,409bp) node { 0};
  \draw [->,solid] (node_2) ..controls (800.88bp,279.54bp) and (835.16bp,290.28bp)  .. (864.65bp,304bp) .. controls (877.72bp,310.08bp) and (878.31bp,316.51bp)  .. (891.65bp,322bp) .. controls (930.17bp,337.86bp) and (957.17bp,307.83bp)  .. (983.65bp,340bp) .. controls (995.51bp,354.41bp) and (995.94bp,367.95bp)  .. (983.65bp,382bp) .. controls (944.09bp,427.23bp) and (889.21bp,354.77bp)  .. (849.65bp,400bp) .. controls (844.38bp,406.02bp) and (844.24bp,412.11bp)  .. (849.65bp,418bp) .. controls (881.48bp,452.66bp) and (1019bp,414.04bp)  .. (1060.6bp,436bp) .. controls (1091.1bp,452.07bp) and (1081.3bp,476.53bp)  .. (1109.6bp,496bp) .. controls (1130.9bp,510.55bp) and (1149.6bp,493.18bp)  .. (1164.6bp,514bp) .. controls (1169.3bp,520.48bp) and (1169.8bp,525.87bp)  .. (1164.6bp,532bp) .. controls (1142.6bp,558.33bp) and (1046bp,566.89bp)  .. (node_18);
  \draw (916.65bp,409bp) node { ($l_G$, $u_G$, $\lambda_G$)};
  \draw [->,solid] (node_18) ..controls (999.92bp,562.32bp) and (1026.7bp,552.6bp)  .. (1040.6bp,532bp) .. controls (1047.6bp,521.72bp) and (1044.5bp,509.84bp)  .. (node_5);
  \draw (1102.6bp,523bp) node { min(D,wtr4+1)};
  \draw [->,solid] (node_0) ..controls (262.14bp,230.25bp) and (274.64bp,220.79bp)  .. (282.65bp,208bp) .. controls (287.37bp,200.47bp) and (288.77bp,191.2bp)  .. (node_16);
  \draw (353.65bp,199bp) node { ($l_C$, $u_C$, $\lambda_C$)};
  \draw [->,solid] (node_6) ..controls (884.99bp,498.11bp) and (892.8bp,506.21bp)  .. (899.65bp,514bp) .. controls (907.36bp,522.77bp) and (915.3bp,532.73bp)  .. (node_18);
  \draw (937.65bp,523bp) node { $wob_2$};
  \draw [->,solid] (node_10) ..controls (1184.6bp,438.31bp) and (1175.7bp,428.94bp)  .. (1170.6bp,418bp) .. controls (1165.9bp,407.73bp) and (1170bp,397.83bp)  .. (node_13);
  \draw (1181.6bp,409bp) node { w};
  \draw [->,solid] (node_18) ..controls (820.66bp,567.2bp) and (587.55bp,557.38bp)  .. (564.65bp,532bp) .. controls (551.56bp,517.5bp) and (561.64bp,504.71bp)  .. (node_1);
  \draw (625.15bp,523bp) node { ($l_B$,$u_B$,$\lambda_B$)};
  \draw [->,solid] (node_18) ..controls (1047.3bp,562.87bp) and (1200.9bp,548.8bp)  .. (1217.6bp,532bp) .. controls (1224.6bp,525bp) and (1227.9bp,515.33bp)  .. (node_10);
  \draw (1285.6bp,523bp) node { min(D,wtr1+1)};
  \draw [->,solid] (node_3) ..controls (188.81bp,505.35bp) and (183.22bp,521.01bp)  .. (193.65bp,532bp) .. controls (218.03bp,557.68bp) and (741.2bp,567.86bp)  .. (node_18);
  \draw (217.65bp,523bp) node { $wob_1$};
  \draw [->,solid] (node_8) ..controls (396.05bp,487.39bp) and (426.46bp,499.5bp)  .. (451.65bp,514bp) .. controls (462.9bp,520.48bp) and (462.56bp,527.26bp)  .. (474.65bp,532bp) .. controls (551.24bp,562.02bp) and (797.54bp,568.94bp)  .. (node_18);
  \draw (496.15bp,523bp) node { wtr3};
  \draw [->,solid] (node_2) ..controls (603.62bp,284.63bp) and (580.21bp,300.7bp)  .. (595.65bp,322bp) .. controls (599.35bp,327.11bp) and (607.48bp,331.9bp)  .. (node_19);
  \draw (662.65bp,313bp) node { ($l_G$, $u_G$, $\lambda_G$)};
  \draw [->,solid] (node_18) ..controls (780.96bp,568.75bp) and (332.56bp,560.39bp)  .. (275.65bp,532bp) .. controls (262.23bp,525.31bp) and (250.76bp,513.8bp)  .. (node_3);
  \draw (299.65bp,523bp) node { $wob_1$};
  \draw [->,solid] (node_7) ..controls (546.54bp,78.888bp) and (550.82bp,86.418bp)  .. (553.65bp,94bp) .. controls (565.76bp,126.53bp) and (563.61bp,137.8bp)  .. (557.65bp,172bp) .. controls (545.47bp,241.8bp) and (556.13bp,274.39bp)  .. (503.65bp,322bp) .. controls (479.54bp,343.87bp) and (452.64bp,314.31bp)  .. (432.65bp,340bp) .. controls (421.18bp,354.73bp) and (420.83bp,367.55bp)  .. (432.65bp,382bp) .. controls (458.2bp,413.24bp) and (485.18bp,382.71bp)  .. (521.65bp,400bp) .. controls (533.06bp,405.41bp) and (531.86bp,413.46bp)  .. (543.65bp,418bp) .. controls (581.44bp,432.55bp) and (876.16bp,410.54bp)  .. (907.65bp,436bp) .. controls (929.11bp,453.35bp) and (905.59bp,475.13bp)  .. (923.65bp,496bp) .. controls (936.93bp,511.36bp) and (954.47bp,497.05bp)  .. (965.65bp,514bp) .. controls (971.02bp,522.15bp) and (969.69bp,531.81bp)  .. (node_18);
  \draw (543.15bp,313bp) node { wtr2};
  \draw [->,solid] (node_9) ..controls (1403.9bp,617.6bp) and (1410.9bp,571.91bp)  .. (1413.6bp,532bp) .. controls (1414.2bp,524.02bp) and (1414.3bp,521.98bp)  .. (1413.6bp,514bp) .. controls (1410.3bp,470.95bp) and (1404.2bp,460.82bp)  .. (1398.6bp,418bp) .. controls (1392bp,367.48bp) and (1398bp,353.66bp)  .. (1386.6bp,304bp) .. controls (1374.6bp,251.51bp) and (1385.1bp,226.68bp)  .. (1345.6bp,190bp) .. controls (1340bp,184.73bp) and (1329bp,179.73bp)  .. (node_14);
  \draw (1409.6bp,409bp) node { w};
  \draw [->,solid] (node_12) ..controls (1091.3bp,220.35bp) and (1078.5bp,205.47bp)  .. (1089.6bp,190bp) .. controls (1093.3bp,184.93bp) and (1101.4bp,180.14bp)  .. (node_14);
  \draw (1153.1bp,199bp) node { ($l_P$, $u_P$, $\lambda_P$)};
  \draw [->,solid] (node_18) ..controls (887.94bp,562.18bp) and (861.41bp,552.45bp)  .. (847.65bp,532bp) .. controls (842.37bp,524.17bp) and (840.9bp,514.55bp)  .. (node_6);
  \draw (871.65bp,523bp) node { $wob_2$};
%
\end{tikzpicture}
% End of code
}}




\section{Repressilator}\label{app:repr}

Another example that is easily expressible with \andy is the
repressilator \cite{Elowitz}.  It is a synthetic genetic regulatory
network consisting of three genes connected in a feedback loop, such
that each gene inhibits the next gene and is inhibited by the previous
one. The repressilator exhibits a stable oscillation with fixed time
periods.
%%
We model it in \andy with three entities $\entities =\{s_1, s_2, s_3\}$
each with two levels representing an \emph{on}/\emph{off} state. Level
$1=on$ for all entities has decay time $\life_{s_i}(1)=1$; the set of
\potential activities is (no \obligatory activity are required):
%
\[
\begin{array}{c}
 r_1: \activ{\emptyset}{s_1}{1}{s_2}\\
 r_2: \activ{\emptyset}{s_2}{1}{s_3}\\
 r_3: \activ{\emptyset}{s_3}{1}{s_1}\\
\end{array}
\]
%
The SNAKES rendering of the repressilator is given in Figure~\ref{fig:repress}.

\begin{figure}
{\centering
\includegraphics[width=\textwidth]{repress.png}}
\caption{Petri net representation of the repressilator with Snakes}\label{fig:repress}
\end{figure}

Figure~\ref{fig:mgsB} shows the complete state graph where we identify
the characteristic oscillating behavior of the repressilator
(represented by cycles). However, notice that there are also paths
that leave the cycles to return into state $3$ where the 3 entities are
not expressed (level $0$). 

\begin{figure}[ht]
\begin{center}
\includegraphics[width=.5\textwidth]{B.pdf}
\end{center}
\caption{State graph of the repressilator}\label{fig:mgsB}
\end{figure}

In order to have a better understanding of these unexpected behaviors,
we use the MGS tool to generate the alternative state graph given
Figure~\ref{fig:mgsA} representing the time progression. In fact, in
this graph, each arc corresponds to a clock tick (phase
Ph.~\ref{item:clock}) followed by a composition of \potential
activities (phase Ph.~\ref{item:reaction}).
%%
The periodic behavior is clearly restricted to a subgraph (bold
cluster on Figure~\ref{fig:mgsA}); the other cluster (dashed on
Figure~\ref{fig:mgsA}) gathers the unexpected states.
%%
After analysing this graph, transitions going from the periodic
cluster to the other corresponds to evolutions with only time
progression and decay without any activity. It may be interpreted as
those cases that are unlikely to happen but still (at least in
principle) plausible which may explain the lack of robustness of such
a synthetic genetic regulatory network when  implemented in real scenarios.

\begin{figure}[ht]
\includegraphics[width=\textwidth]{A.pdf}
\caption{Time progression in the repressilator state space}\label{fig:mgsA}
\end{figure}

%% Moreover we have studied its state space with MGS obtaining a graph
%% that shows the periodic behavior typical of the repressilator. Figure
%% \ref{fig:mgsB} shows an extract of the complete state space where we
%% identify the oscillation (represented by cycles). In the complete
%% graph (Figure \ref{fig:mgsA}) notice that there are also paths that
%% leave the cycles. This corresponds to evolutions with only time
%% progression and decay without any activity and it may be interpreted
%% as those cases that are unlikely to happen but still (at least in
%% principle) plausible.  Thus the model is suitable to address
%% robustness matters as we can test the model against the appearance of
%% even the less likely to occur events.

%% \begin{figure}[ht]
%% \includegraphics[width=\textwidth]{B.pdf}
%% \caption{Extract of the state space of the repressilator}\label{fig:mgsB}
%% \end{figure}



\end{document}


CAMBIARE L DEGLI AUTOMI IN L CALLIGRAFICO SI CONFONDE CON GLI L DEI LIVELLI


COMMENTAIRE A CONSIDERER POUR UNE VERSION PLUS LONGUE



\comment{%
        Initialement on disait : ``chaque entité possède un ensemble
        d'attributs'', ce qui n'est pas le cas vu la formalisation. Si
        une entité possède un seul attribut, alors il vaut peut-être
        mieux parler de \emph{variable} ou d'\emph{observable} que
        d'entité (car on parle des variables ou des observables d'un
        système et qu'habituelement une entité/objet est caractérisé par
        plusieurs attributs): ``a measurable property of a physical
        system''. %
      }



\comment{%%
  Why restraining to decay? For instance, with this formalism,
  I cannot fill in a bathtub. 

  Using an arbitrary $d_\entity$ for the evolution of the state of
  $\entity$ subsumes both increase and decrease. Note also that it
  simplifies greatly the modeling of a \emph{clock}: it is enough to
  consider a $d_\entity$ with a limit cycle. Note that this does not
  prevent to check that $d_\entity$ is monotonic (that is, induce a
  strict order on $\setlev$ when $x \leq d_\entity(x)$ for all $x \in
  \setlev$) and to use this property in the tools (\eg to cut
  the state space).  %%
} %%



\comment{%%
  Again: we can have states that are not levels. It will extend at no
  cost the applicability of the formalism. The decreasing function on
  levels can be modeled by a map $d_\entity : \setlev \mapsto \setlev$. We can
  insists to have an infinite delay for the fixed points $x$ of $d_\entity :
  \life_\entity(x) = \omega \Leftrightarrow d_\entity(x) = x$ and that
  $\level{\entity}$ is a fixed point. 
  %% 
}



 \comment{%%
  The purpose/use of $v$ must be given here. %%
  To generalize decay, replace $v \in \mathbb{Z}$ by $d : \setlev_\entity
  \mapsto \setlev_\entity$ and the addition/subtraction by the
  application of $d$. Think to $d$ as the successor/predecessor
  function. Requiring $d$ \emph{injective} to have $d^{-1}$ is to strong
  because of the fixed points. What is the weakest relevant
  assumption?  %%
}


\comment{%%
  Why is the discharge not related to the duration of the call? How to
  model it?
        
  If the phone is plugged, it does not discharge when there is a phone
  call.  %%
} 
